1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_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
43 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
45 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
47 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
48 datatype type_heaviness = Heavyweight | Lightweight
51 Simple_Types of type_level |
52 Preds of polymorphism * type_level * type_heaviness |
53 Tags of polymorphism * type_level * type_heaviness
55 type translated_formula
57 val bound_var_prefix : string
58 val schematic_var_prefix: string
59 val fixed_var_prefix: string
60 val tvar_prefix: string
61 val tfree_prefix: string
62 val const_prefix: string
63 val type_const_prefix: string
64 val class_prefix: string
65 val skolem_const_prefix : string
66 val old_skolem_const_prefix : string
67 val new_skolem_const_prefix : string
68 val type_decl_prefix : string
69 val sym_decl_prefix : string
70 val preds_sym_formula_prefix : string
71 val lightweight_tags_sym_formula_prefix : string
72 val fact_prefix : string
73 val conjecture_prefix : string
74 val helper_prefix : string
75 val class_rel_clause_prefix : string
76 val arity_clause_prefix : string
77 val tfree_clause_prefix : string
78 val typed_helper_suffix : string
79 val untyped_helper_suffix : string
80 val type_tag_idempotence_helper_name : string
81 val predicator_name : string
82 val app_op_name : string
83 val type_tag_name : string
84 val type_pred_name : string
85 val simple_type_prefix : string
86 val prefixed_predicator_name : string
87 val prefixed_app_op_name : string
88 val prefixed_type_tag_name : string
89 val ascii_of: string -> string
90 val unascii_of: string -> string
91 val strip_prefix_and_unascii : string -> string -> string option
92 val proxy_table : (string * (string * (thm * (string * string)))) list
93 val proxify_const : string -> (string * string) option
94 val invert_const: string -> string
95 val unproxify_const: string -> string
96 val make_bound_var : string -> string
97 val make_schematic_var : string * int -> string
98 val make_fixed_var : string -> string
99 val make_schematic_type_var : string * int -> string
100 val make_fixed_type_var : string -> string
101 val make_fixed_const : string -> string
102 val make_fixed_type_const : string -> string
103 val make_type_class : string -> string
104 val new_skolem_var_name_from_const : string -> string
105 val num_type_args : theory -> string -> int
106 val make_arity_clauses :
107 theory -> string list -> class list -> class list * arity_clause list
108 val make_class_rel_clauses :
109 theory -> class list -> class list -> class_rel_clause list
110 val combtyp_of : combterm -> typ
111 val strip_combterm_comb : combterm -> combterm * combterm list
112 val atyps_of : typ -> typ list
113 val combterm_from_term :
114 theory -> (string * typ) list -> term -> combterm * typ list
115 val is_locality_global : locality -> bool
116 val type_sys_from_string : string -> type_sys
117 val polymorphism_of_type_sys : type_sys -> polymorphism
118 val level_of_type_sys : type_sys -> type_level
119 val is_type_sys_virtually_sound : type_sys -> bool
120 val is_type_sys_fairly_sound : type_sys -> bool
121 val choose_format : format list -> type_sys -> format * type_sys
122 val raw_type_literals_for_types : typ list -> type_literal list
124 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
125 val unmangled_const_name : string -> string
126 val unmangled_const : string -> string * string fo_term list
127 val translate_atp_fact :
128 Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
129 -> translated_formula option * ((string * locality) * thm)
130 val helper_table : ((string * bool) * thm list) list
131 val should_specialize_helper : type_sys -> term -> bool
132 val tfree_classes_of_terms : term list -> string list
133 val tvar_classes_of_terms : term list -> string list
134 val type_constrs_of_terms : theory -> term list -> string list
135 val prepare_atp_problem :
136 Proof.context -> format -> formula_kind -> formula_kind -> type_sys
137 -> bool option -> bool -> bool -> term list -> term
138 -> (translated_formula option * ((string * 'a) * thm)) list
139 -> string problem * string Symtab.table * int * int
140 * (string * 'a) list vector * int list * int Symtab.table
141 val atp_problem_weights : string problem -> (string * real) list
144 structure ATP_Translate : ATP_TRANSLATE =
150 type name = string * string
153 fun union_all xss = fold (union (op =)) xss []
156 val generate_useful_info = false
158 fun useful_isabelle_info s =
159 if generate_useful_info then
160 SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
164 val intro_info = useful_isabelle_info "intro"
165 val elim_info = useful_isabelle_info "elim"
166 val simp_info = useful_isabelle_info "simp"
168 val bound_var_prefix = "B_"
169 val schematic_var_prefix = "V_"
170 val fixed_var_prefix = "v_"
172 val tvar_prefix = "T_"
173 val tfree_prefix = "t_"
175 val const_prefix = "c_"
176 val type_const_prefix = "tc_"
177 val class_prefix = "cl_"
179 val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
180 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
181 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
183 val type_decl_prefix = "ty_"
184 val sym_decl_prefix = "sy_"
185 val preds_sym_formula_prefix = "psy_"
186 val lightweight_tags_sym_formula_prefix = "tsy_"
187 val fact_prefix = "fact_"
188 val conjecture_prefix = "conj_"
189 val helper_prefix = "help_"
190 val class_rel_clause_prefix = "clar_"
191 val arity_clause_prefix = "arity_"
192 val tfree_clause_prefix = "tfree_"
194 val typed_helper_suffix = "_T"
195 val untyped_helper_suffix = "_U"
196 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
198 val predicator_name = "hBOOL"
199 val app_op_name = "hAPP"
200 val type_tag_name = "ti"
201 val type_pred_name = "is"
202 val simple_type_prefix = "ty_"
204 val prefixed_predicator_name = const_prefix ^ predicator_name
205 val prefixed_app_op_name = const_prefix ^ app_op_name
206 val prefixed_type_tag_name = const_prefix ^ type_tag_name
208 (* Freshness almost guaranteed! *)
209 val sledgehammer_weak_prefix = "Sledgehammer:"
211 (*Escaping of special characters.
212 Alphanumeric characters are left unchanged.
213 The character _ goes to __
214 Characters in the range ASCII space to / go to _A to _P, respectively.
215 Other characters go to _nnn where nnn is the decimal ASCII code.*)
216 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
218 fun stringN_of_int 0 _ = ""
219 | stringN_of_int k n =
220 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
222 fun ascii_of_char c =
223 if Char.isAlphaNum c then
225 else if c = #"_" then
227 else if #" " <= c andalso c <= #"/" then
228 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
230 (* fixed width, in case more digits follow *)
231 "_" ^ stringN_of_int 3 (Char.ord c)
233 val ascii_of = String.translate ascii_of_char
235 (** Remove ASCII armoring from names in proof files **)
237 (* We don't raise error exceptions because this code can run inside a worker
238 thread. Also, the errors are impossible. *)
241 fun un rcs [] = String.implode(rev rcs)
242 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
243 (* Three types of _ escapes: __, _A to _P, _nnn *)
244 | un rcs (#"_" :: #"_" :: cs) = un (#"_"::rcs) cs
245 | un rcs (#"_" :: c :: cs) =
246 if #"A" <= c andalso c<= #"P" then
247 (* translation of #" " to #"/" *)
248 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
250 let val digits = List.take (c::cs, 3) handle Subscript => [] in
251 case Int.fromString (String.implode digits) of
252 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
253 | NONE => un (c:: #"_"::rcs) cs (* ERROR *)
255 | un rcs (c :: cs) = un (c :: rcs) cs
256 in un [] o String.explode end
258 (* If string s has the prefix s1, return the result of deleting it,
260 fun strip_prefix_and_unascii s1 s =
261 if String.isPrefix s1 s then
262 SOME (unascii_of (String.extract (s, size s1, NONE)))
267 [("c_False", (@{const_name False}, (@{thm fFalse_def},
268 ("fFalse", @{const_name ATP.fFalse})))),
269 ("c_True", (@{const_name True}, (@{thm fTrue_def},
270 ("fTrue", @{const_name ATP.fTrue})))),
271 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
272 ("fNot", @{const_name ATP.fNot})))),
273 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
274 ("fconj", @{const_name ATP.fconj})))),
275 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
276 ("fdisj", @{const_name ATP.fdisj})))),
277 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
278 ("fimplies", @{const_name ATP.fimplies})))),
279 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
280 ("fequal", @{const_name ATP.fequal}))))]
282 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
284 (* Readable names for the more common symbolic functions. Do not mess with the
285 table unless you know what you are doing. *)
286 val const_trans_table =
287 [(@{type_name Product_Type.prod}, "prod"),
288 (@{type_name Sum_Type.sum}, "sum"),
289 (@{const_name False}, "False"),
290 (@{const_name True}, "True"),
291 (@{const_name Not}, "Not"),
292 (@{const_name conj}, "conj"),
293 (@{const_name disj}, "disj"),
294 (@{const_name implies}, "implies"),
295 (@{const_name HOL.eq}, "equal"),
296 (@{const_name If}, "If"),
297 (@{const_name Set.member}, "member"),
298 (@{const_name Meson.COMBI}, "COMBI"),
299 (@{const_name Meson.COMBK}, "COMBK"),
300 (@{const_name Meson.COMBB}, "COMBB"),
301 (@{const_name Meson.COMBC}, "COMBC"),
302 (@{const_name Meson.COMBS}, "COMBS")]
304 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
306 (* Invert the table of translations between Isabelle and ATPs. *)
307 val const_trans_table_inv =
308 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
309 val const_trans_table_unprox =
311 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
313 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
314 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
317 case Symtab.lookup const_trans_table c of
321 (*Remove the initial ' character from a type variable, if it is present*)
322 fun trim_type_var s =
323 if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
324 else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
326 fun ascii_of_indexname (v,0) = ascii_of v
327 | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i
329 fun make_bound_var x = bound_var_prefix ^ ascii_of x
330 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
331 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
333 fun make_schematic_type_var (x,i) =
334 tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i))
335 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))
337 (* HOL.eq MUST BE "equal" because it's built into ATPs. *)
338 fun make_fixed_const @{const_name HOL.eq} = "equal"
339 | make_fixed_const c = const_prefix ^ lookup_const c
341 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
343 fun make_type_class clas = class_prefix ^ ascii_of clas
345 fun new_skolem_var_name_from_const s =
346 let val ss = s |> space_explode Long_Name.separator in
347 nth ss (length ss - 2)
350 (* The number of type arguments of a constant, zero if it's monomorphic. For
351 (instances of) Skolem pseudoconstants, this information is encoded in the
353 fun num_type_args thy s =
354 if String.isPrefix skolem_const_prefix s then
355 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
357 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
359 (** Definitions and functions for FOL clauses and formulas for TPTP **)
361 (* The first component is the type class; the second is a "TVar" or "TFree". *)
362 datatype type_literal =
363 TyLitVar of name * name |
364 TyLitFree of name * name
367 (** Isabelle arities **)
369 datatype arity_literal =
370 TConsLit of name * name * name list |
371 TVarLit of name * name
374 | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
376 fun pack_sort (_,[]) = []
377 | pack_sort (tvar, "HOL.type" :: srt) =
378 pack_sort (tvar, srt) (* IGNORE sort "type" *)
379 | pack_sort (tvar, cls :: srt) =
380 (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt)
384 prem_lits: arity_literal list,
385 concl_lits: arity_literal}
387 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
388 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
390 val tvars = gen_TVars (length args)
391 val tvars_srts = ListPair.zip (tvars, args)
394 prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)),
395 concl_lits = TConsLit (`make_type_class cls,
396 `make_fixed_type_const tcons,
400 fun arity_clause _ _ (_, []) = []
401 | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
402 arity_clause seen n (tcons,ars)
403 | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
404 if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
405 make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) ::
406 arity_clause seen (n+1) (tcons,ars)
408 make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
409 arity_clause (class::seen) n (tcons,ars)
411 fun multi_arity_clause [] = []
412 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
413 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
415 (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
416 provided its arguments have the corresponding sorts.*)
417 fun type_class_pairs thy tycons classes =
419 val alg = Sign.classes_of thy
420 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
421 fun add_class tycon class =
422 cons (class, domain_sorts tycon class)
423 handle Sorts.CLASS_ERROR _ => I
424 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
425 in map try_classes tycons end
427 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
428 fun iter_type_class_pairs _ _ [] = ([], [])
429 | iter_type_class_pairs thy tycons classes =
430 let val cpairs = type_class_pairs thy tycons classes
431 val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
432 |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
433 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
434 in (union (op =) classes' classes, union (op =) cpairs' cpairs) end
436 fun make_arity_clauses thy tycons =
437 iter_type_class_pairs thy tycons ##> multi_arity_clause
440 (** Isabelle class relations **)
442 type class_rel_clause =
447 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
448 fun class_pairs _ [] _ = []
449 | class_pairs thy subs supers =
451 val class_less = Sorts.class_less (Sign.classes_of thy)
452 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
453 fun add_supers sub = fold (add_super sub) supers
454 in fold add_supers subs [] end
456 fun make_class_rel_clause (sub,super) =
457 {name = sub ^ "_" ^ super,
458 subclass = `make_type_class sub,
459 superclass = `make_type_class super}
461 fun make_class_rel_clauses thy subs supers =
462 map make_class_rel_clause (class_pairs thy subs supers)
465 CombConst of name * typ * typ list |
466 CombVar of name * typ |
467 CombApp of combterm * combterm
469 fun combtyp_of (CombConst (_, T, _)) = T
470 | combtyp_of (CombVar (_, T)) = T
471 | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
473 (*gets the head of a combinator application, along with the list of arguments*)
474 fun strip_combterm_comb u =
475 let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
479 fun atyps_of T = fold_atyps (insert (op =)) T []
481 fun new_skolem_const_name s num_T_args =
482 [new_skolem_const_prefix, s, string_of_int num_T_args]
483 |> space_implode Long_Name.separator
485 (* Converts a term (with combinators) into a combterm. Also accumulates sort
487 fun combterm_from_term thy bs (P $ Q) =
489 val (P', P_atomics_Ts) = combterm_from_term thy bs P
490 val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
491 in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
492 | combterm_from_term thy _ (Const (c, T)) =
495 (if String.isPrefix old_skolem_const_prefix c then
496 [] |> Term.add_tvarsT T |> map TVar
498 (c, T) |> Sign.const_typargs thy)
499 val c' = CombConst (`make_fixed_const c, T, tvar_list)
500 in (c', atyps_of T) end
501 | combterm_from_term _ _ (Free (v, T)) =
502 (CombConst (`make_fixed_var v, T, []), atyps_of T)
503 | combterm_from_term _ _ (Var (v as (s, _), T)) =
504 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
506 val Ts = T |> strip_type |> swap |> op ::
507 val s' = new_skolem_const_name s (length Ts)
508 in CombConst (`make_fixed_const s', T, Ts) end
510 CombVar ((make_schematic_var v, s), T), atyps_of T)
511 | combterm_from_term _ bs (Bound j) =
513 |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
514 | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
516 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
518 (* (quasi-)underapproximation of the truth *)
519 fun is_locality_global Local = false
520 | is_locality_global Assum = false
521 | is_locality_global Chained = false
522 | is_locality_global _ = true
524 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
525 datatype type_level =
526 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
527 datatype type_heaviness = Heavyweight | Lightweight
530 Simple_Types of type_level |
531 Preds of polymorphism * type_level * type_heaviness |
532 Tags of polymorphism * type_level * type_heaviness
534 fun try_unsuffixes ss s =
535 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
537 fun type_sys_from_string s =
538 (case try (unprefix "poly_") s of
539 SOME s => (SOME Polymorphic, s)
541 case try (unprefix "mono_") s of
542 SOME s => (SOME Monomorphic, s)
544 case try (unprefix "mangled_") s of
545 SOME s => (SOME Mangled_Monomorphic, s)
548 (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
549 case try_unsuffixes ["?", "_query"] s of
550 SOME s => (Nonmonotonic_Types, s)
552 case try_unsuffixes ["!", "_bang"] s of
553 SOME s => (Finite_Types, s)
554 | NONE => (All_Types, s))
556 case try (unsuffix "_heavy") s of
557 SOME s => (Heavyweight, s)
558 | NONE => (Lightweight, s))
559 |> (fn (poly, (level, (heaviness, core))) =>
560 case (core, (poly, level, heaviness)) of
561 ("simple", (NONE, _, Lightweight)) => Simple_Types level
562 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
563 | ("tags", (SOME Polymorphic, All_Types, _)) =>
564 Tags (Polymorphic, All_Types, heaviness)
565 | ("tags", (SOME Polymorphic, _, _)) =>
566 (* The actual light encoding is very unsound. *)
567 Tags (Polymorphic, level, Heavyweight)
568 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
569 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
570 Preds (poly, Const_Arg_Types, Lightweight)
571 | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
572 Preds (Polymorphic, No_Types, Lightweight)
573 | _ => raise Same.SAME)
574 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
576 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
577 | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
578 | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
580 fun level_of_type_sys (Simple_Types level) = level
581 | level_of_type_sys (Preds (_, level, _)) = level
582 | level_of_type_sys (Tags (_, level, _)) = level
584 fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
585 | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
586 | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
588 fun is_type_level_virtually_sound level =
589 level = All_Types orelse level = Nonmonotonic_Types
590 val is_type_sys_virtually_sound =
591 is_type_level_virtually_sound o level_of_type_sys
593 fun is_type_level_fairly_sound level =
594 is_type_level_virtually_sound level orelse level = Finite_Types
595 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
597 fun is_setting_higher_order THF (Simple_Types _) = true
598 | is_setting_higher_order _ _ = false
600 fun choose_format formats (Simple_Types level) =
601 if member (op =) formats THF then (THF, Simple_Types level)
602 else if member (op =) formats TFF then (TFF, Simple_Types level)
603 else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
604 | choose_format formats type_sys =
607 (CNF_UEQ, case type_sys of
609 (if is_type_sys_fairly_sound type_sys then Preds else Tags)
612 | format => (format, type_sys))
614 type translated_formula =
618 combformula: (name, typ, combterm) formula,
619 atomic_types: typ list}
621 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
622 : translated_formula) =
623 {name = name, locality = locality, kind = kind, combformula = f combformula,
624 atomic_types = atomic_types} : translated_formula
626 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
628 val type_instance = Sign.typ_instance o Proof_Context.theory_of
630 fun insert_type ctxt get_T x xs =
631 let val T = get_T x in
632 if exists (curry (type_instance ctxt) T o get_T) xs then xs
633 else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
636 (* The Booleans indicate whether all type arguments should be kept. *)
637 datatype type_arg_policy =
638 Explicit_Type_Args of bool |
639 Mangled_Type_Args of bool |
642 fun should_drop_arg_type_args (Simple_Types _) =
643 false (* since TFF doesn't support overloading *)
644 | should_drop_arg_type_args type_sys =
645 level_of_type_sys type_sys = All_Types andalso
646 heaviness_of_type_sys type_sys = Heavyweight
648 fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
649 | general_type_arg_policy type_sys =
650 if level_of_type_sys type_sys = No_Types then
652 else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
653 Mangled_Type_Args (should_drop_arg_type_args type_sys)
655 Explicit_Type_Args (should_drop_arg_type_args type_sys)
657 fun type_arg_policy type_sys s =
658 if s = @{const_name HOL.eq} orelse
659 (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
661 else if s = type_tag_name then
662 Explicit_Type_Args false
664 general_type_arg_policy type_sys
666 (*Make literals for sorted type variables*)
667 fun generic_sorts_on_type (_, []) = []
668 | generic_sorts_on_type ((x, i), s :: ss) =
669 generic_sorts_on_type ((x, i), ss)
670 |> (if s = the_single @{sort HOL.type} then
673 cons (TyLitFree (`make_type_class s, `make_fixed_type_var x))
675 cons (TyLitVar (`make_type_class s,
676 (make_schematic_type_var (x, i), x))))
677 fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S)
678 | sorts_on_tfree _ = []
679 fun sorts_on_tvar (TVar z) = generic_sorts_on_type z
680 | sorts_on_tvar _ = []
682 (* Given a list of sorted type variables, return a list of type literals. *)
683 fun raw_type_literals_for_types Ts =
684 union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)
686 fun type_literals_for_types type_sys sorts_on_typ Ts =
687 if level_of_type_sys type_sys = No_Types then []
688 else union_all (map sorts_on_typ Ts)
690 fun mk_aconns c phis =
691 let val (phis', phi') = split_last phis in
692 fold_rev (mk_aconn c) phis' phi'
694 fun mk_ahorn [] phi = phi
695 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
696 fun mk_aquant _ [] phi = phi
697 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
698 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
699 | mk_aquant q xs phi = AQuant (q, xs, phi)
701 fun close_universally atom_vars phi =
703 fun formula_vars bounds (AQuant (_, xs, phi)) =
704 formula_vars (map fst xs @ bounds) phi
705 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
706 | formula_vars bounds (AAtom tm) =
707 union (op =) (atom_vars tm []
708 |> filter_out (member (op =) bounds o fst))
709 in mk_aquant AForall (formula_vars [] phi []) phi end
711 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
712 | combterm_vars (CombConst _) = I
713 | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
714 fun close_combformula_universally phi = close_universally combterm_vars phi
716 fun term_vars (ATerm (name as (s, _), tms)) =
717 is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
718 fun close_formula_universally phi = close_universally term_vars phi
720 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
721 val homo_infinite_type = Type (homo_infinite_type_name, [])
723 fun fo_term_from_typ format type_sys =
725 fun term (Type (s, Ts)) =
726 ATerm (case (is_setting_higher_order format type_sys, s) of
727 (true, @{type_name bool}) => `I tptp_bool_type
728 | (true, @{type_name fun}) => `I tptp_fun_type
729 | _ => if s = homo_infinite_type_name andalso
730 (format = TFF orelse format = THF) then
731 `I tptp_individual_type
733 `make_fixed_type_const s,
735 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
736 | term (TVar ((x as (s, _)), _)) =
737 ATerm ((make_schematic_type_var x, s), [])
740 (* This shouldn't clash with anything else. *)
741 val mangled_type_sep = "\000"
743 fun generic_mangled_type_name f (ATerm (name, [])) = f name
744 | generic_mangled_type_name f (ATerm (name, tys)) =
745 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
748 val bool_atype = AType (`I tptp_bool_type)
750 fun make_simple_type s =
751 if s = tptp_bool_type orelse s = tptp_fun_type orelse
752 s = tptp_individual_type then
755 simple_type_prefix ^ ascii_of s
757 fun ho_type_from_fo_term format type_sys pred_sym ary =
760 AType ((make_simple_type (generic_mangled_type_name fst ty),
761 generic_mangled_type_name snd ty))
762 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
763 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
764 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
765 fun to_ho (ty as ATerm ((s, _), tys)) =
766 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
767 in if is_setting_higher_order format type_sys then to_ho else to_fo ary end
769 fun mangled_type format type_sys pred_sym ary =
770 ho_type_from_fo_term format type_sys pred_sym ary
771 o fo_term_from_typ format type_sys
773 fun mangled_const_name format type_sys T_args (s, s') =
775 val ty_args = map (fo_term_from_typ format type_sys) T_args
776 fun type_suffix f g =
777 fold_rev (curry (op ^) o g o prefix mangled_type_sep
778 o generic_mangled_type_name f) ty_args ""
779 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
781 val parse_mangled_ident =
782 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
784 fun parse_mangled_type x =
786 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
788 and parse_mangled_types x =
789 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
791 fun unmangled_type s =
792 s |> suffix ")" |> raw_explode
793 |> Scan.finite Symbol.stopper
794 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
795 quote s)) parse_mangled_type))
798 val unmangled_const_name = space_explode mangled_type_sep #> hd
799 fun unmangled_const s =
800 let val ss = space_explode mangled_type_sep s in
801 (hd ss, map unmangled_type (tl ss))
804 fun introduce_proxies format type_sys =
806 fun intro top_level (CombApp (tm1, tm2)) =
807 CombApp (intro top_level tm1, intro false tm2)
808 | intro top_level (CombConst (name as (s, _), T, T_args)) =
809 (case proxify_const s of
811 if top_level orelse is_setting_higher_order format type_sys then
812 case (top_level, s) of
813 (_, "c_False") => (`I tptp_false, [])
814 | (_, "c_True") => (`I tptp_true, [])
815 | (false, "c_Not") => (`I tptp_not, [])
816 | (false, "c_conj") => (`I tptp_and, [])
817 | (false, "c_disj") => (`I tptp_or, [])
818 | (false, "c_implies") => (`I tptp_implies, [])
820 if is_tptp_equal s then (`I tptp_equal, [])
821 else (proxy_base |>> prefix const_prefix, T_args)
824 (proxy_base |>> prefix const_prefix, T_args)
825 | NONE => (name, T_args))
826 |> (fn (name, T_args) => CombConst (name, T, T_args))
830 fun combformula_from_prop thy format type_sys eq_as_iff =
832 fun do_term bs t atomic_types =
833 combterm_from_term thy bs (Envir.eta_contract t)
834 |>> (introduce_proxies format type_sys #> AAtom)
835 ||> union (op =) atomic_types
836 fun do_quant bs q s T t' =
837 let val s = Name.variant (map fst bs) s in
838 do_formula ((s, T) :: bs) t'
839 #>> mk_aquant q [(`make_bound_var s, SOME T)]
841 and do_conn bs c t1 t2 =
842 do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
843 and do_formula bs t =
845 @{const Trueprop} $ t1 => do_formula bs t1
846 | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
847 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
848 do_quant bs AForall s T t'
849 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
850 do_quant bs AExists s T t'
851 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
852 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
853 | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
854 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
855 if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
859 fun presimplify_term ctxt =
860 Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
861 #> Meson.presimplify ctxt
864 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
865 fun conceal_bounds Ts t =
866 subst_bounds (map (Free o apfst concealed_bound_name)
867 (0 upto length Ts - 1 ~~ Ts), t)
868 fun reveal_bounds Ts =
869 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
870 (0 upto length Ts - 1 ~~ Ts))
872 fun extensionalize_term ctxt t =
873 let val thy = Proof_Context.theory_of ctxt in
874 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
875 |> prop_of |> Logic.dest_equals |> snd
878 fun introduce_combinators_in_term ctxt kind t =
879 let val thy = Proof_Context.theory_of ctxt in
880 if Meson.is_fol_term thy t then
886 @{const Not} $ t1 => @{const Not} $ aux Ts t1
887 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
888 t0 $ Abs (s, T, aux (T :: Ts) t')
889 | (t0 as Const (@{const_name All}, _)) $ t1 =>
890 aux Ts (t0 $ eta_expand Ts t1 1)
891 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
892 t0 $ Abs (s, T, aux (T :: Ts) t')
893 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
894 aux Ts (t0 $ eta_expand Ts t1 1)
895 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
896 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
897 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
898 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
900 t0 $ aux Ts t1 $ aux Ts t2
901 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
904 t |> conceal_bounds Ts
905 |> Envir.eta_contract
907 |> Meson_Clausify.introduce_combinators_in_cterm
908 |> prop_of |> Logic.dest_equals |> snd
910 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
911 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
913 (* A type variable of sort "{}" will make abstraction fail. *)
914 if kind = Conjecture then HOLogic.false_const
915 else HOLogic.true_const
918 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
919 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
922 fun aux (t $ u) = aux t $ aux u
923 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
924 | aux (Var ((s, i), T)) =
925 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
927 in t |> exists_subterm is_Var t ? aux end
929 fun preprocess_prop ctxt presimp kind t =
931 val thy = Proof_Context.theory_of ctxt
932 val t = t |> Envir.beta_eta_contract
933 |> transform_elim_prop
934 |> Object_Logic.atomize_term thy
935 val need_trueprop = (fastype_of t = @{typ bool})
937 t |> need_trueprop ? HOLogic.mk_Trueprop
938 |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
939 |> extensionalize_term ctxt
940 |> presimp ? presimplify_term ctxt
941 |> perhaps (try (HOLogic.dest_Trueprop))
942 |> introduce_combinators_in_term ctxt kind
945 (* making fact and conjecture formulas *)
946 fun make_formula thy format type_sys eq_as_iff name loc kind t =
948 val (combformula, atomic_types) =
949 combformula_from_prop thy format type_sys eq_as_iff t []
951 {name = name, locality = loc, kind = kind, combformula = combformula,
952 atomic_types = atomic_types}
955 fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp
957 let val thy = Proof_Context.theory_of ctxt in
959 t |> preproc ? preprocess_prop ctxt presimp Axiom
960 |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
962 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
963 if s = tptp_true then NONE else SOME formula
964 | (_, formula) => SOME formula
967 fun make_conjecture ctxt format prem_kind type_sys preproc ts =
969 val thy = Proof_Context.theory_of ctxt
970 val last = length ts - 1
972 map2 (fn j => fn t =>
974 val (kind, maybe_negate) =
979 if prem_kind = Conjecture then update_combformula mk_anot
982 t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
983 |> make_formula thy format type_sys (format <> CNF)
984 (string_of_int j) General kind
990 (** Finite and infinite type inference **)
992 fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
993 | deep_freeze_atyp T = T
994 val deep_freeze_type = map_atyps deep_freeze_atyp
996 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
997 dangerous because their "exhaust" properties can easily lead to unsound ATP
998 proofs. On the other hand, all HOL infinite types can be given the same
999 models in first-order logic (via Löwenheim-Skolem). *)
1001 fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
1002 exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
1003 | should_encode_type _ _ All_Types _ = true
1004 | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
1005 | should_encode_type _ _ _ _ = false
1007 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
1008 should_predicate_on_var T =
1009 (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
1010 should_encode_type ctxt nonmono_Ts level T
1011 | should_predicate_on_type _ _ _ _ _ = false
1013 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
1014 String.isPrefix bound_var_prefix s
1015 | is_var_or_bound_var (CombVar _) = true
1016 | is_var_or_bound_var _ = false
1018 datatype tag_site = Top_Level | Eq_Arg | Elsewhere
1020 fun should_tag_with_type _ _ _ Top_Level _ _ = false
1021 | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
1023 Heavyweight => should_encode_type ctxt nonmono_Ts level T
1025 case (site, is_var_or_bound_var u) of
1026 (Eq_Arg, true) => 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',
1063 fold (fn T' => consider_var_arity T' T) types min_ary,
1064 max_ary = max_ary, types = types}
1066 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1068 if bool_vars' = bool_vars andalso
1069 pointer_eq (fun_var_Ts', fun_var_Ts) then
1072 ((bool_vars', fun_var_Ts'),
1073 Symtab.map (K repair_min_arity) sym_tab)
1077 fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1078 let val (head, args) = strip_combterm_comb tm in
1080 CombConst ((s, _), T, _) =>
1081 if String.isPrefix bound_var_prefix s then
1082 add_var_or_bound_var T accum
1084 let val ary = length args in
1085 ((bool_vars, fun_var_Ts),
1086 case Symtab.lookup sym_tab s of
1087 SOME {pred_sym, min_ary, max_ary, types} =>
1090 pred_sym andalso top_level andalso not bool_vars
1091 val types' = types |> insert_type ctxt I T
1093 if is_some explicit_apply orelse
1094 pointer_eq (types', types) then
1097 fold (consider_var_arity T) fun_var_Ts min_ary
1099 Symtab.update (s, {pred_sym = pred_sym,
1100 min_ary = Int.min (ary, min_ary),
1101 max_ary = Int.max (ary, max_ary),
1107 val pred_sym = top_level andalso not bool_vars
1109 case explicit_apply of
1112 | NONE => fold (consider_var_arity T) fun_var_Ts ary
1114 Symtab.update_new (s, {pred_sym = pred_sym,
1115 min_ary = min_ary, max_ary = ary,
1120 | CombVar (_, T) => add_var_or_bound_var T accum
1122 |> fold (add false) args
1125 fun add_fact_syms_to_table ctxt explicit_apply =
1126 fact_lift (formula_fold NONE
1127 (K (add_combterm_syms_to_table ctxt explicit_apply)))
1129 val default_sym_tab_entries : (string * sym_info) list =
1130 (prefixed_predicator_name,
1131 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
1132 ([tptp_false, tptp_true]
1133 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
1134 ([tptp_equal, tptp_old_equal]
1135 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
1137 fun sym_table_for_facts ctxt explicit_apply facts =
1138 ((false, []), Symtab.empty)
1139 |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
1140 |> fold Symtab.update default_sym_tab_entries
1142 fun min_arity_of sym_tab s =
1143 case Symtab.lookup sym_tab s of
1144 SOME ({min_ary, ...} : sym_info) => min_ary
1146 case strip_prefix_and_unascii const_prefix s of
1148 let val s = s |> unmangled_const_name |> invert_const in
1149 if s = predicator_name then 1
1150 else if s = app_op_name then 2
1151 else if s = type_pred_name then 1
1156 (* True if the constant ever appears outside of the top-level position in
1157 literals, or if it appears with different arities (e.g., because of different
1158 type instantiations). If false, the constant always receives all of its
1159 arguments and is used as a predicate. *)
1160 fun is_pred_sym sym_tab s =
1161 case Symtab.lookup sym_tab s of
1162 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1163 pred_sym andalso min_ary = max_ary
1166 val predicator_combconst =
1167 CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
1168 fun predicator tm = CombApp (predicator_combconst, tm)
1170 fun introduce_predicators_in_combterm sym_tab tm =
1171 case strip_combterm_comb tm of
1172 (CombConst ((s, _), _, _), _) =>
1173 if is_pred_sym sym_tab s then tm else predicator tm
1174 | _ => predicator tm
1176 fun list_app head args = fold (curry (CombApp o swap)) args head
1178 val app_op = `make_fixed_const app_op_name
1180 fun explicit_app arg head =
1182 val head_T = combtyp_of head
1183 val (arg_T, res_T) = dest_funT head_T
1185 CombConst (app_op, head_T --> head_T, [arg_T, res_T])
1186 in list_app explicit_app [head, arg] end
1187 fun list_explicit_app head args = fold explicit_app args head
1189 fun introduce_explicit_apps_in_combterm sym_tab =
1192 case strip_combterm_comb tm of
1193 (head as CombConst ((s, _), _, _), args) =>
1195 |> chop (min_arity_of sym_tab s)
1197 |-> list_explicit_app
1198 | (head, args) => list_explicit_app head (map aux args)
1201 fun chop_fun 0 T = ([], T)
1202 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1203 chop_fun (n - 1) ran_T |>> cons dom_T
1204 | chop_fun _ _ = raise Fail "unexpected non-function"
1206 fun filter_type_args _ _ _ [] = []
1207 | filter_type_args thy s arity T_args =
1209 (* will throw "TYPE" for pseudo-constants *)
1210 val U = if s = app_op_name then
1211 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
1213 s |> Sign.the_const_type thy
1215 case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
1218 let val U_args = (s, U) |> Sign.const_typargs thy in
1220 |> map_filter (fn (U, T) =>
1221 if member (op =) res_U_vars (dest_TVar U) then
1227 handle TYPE _ => T_args
1229 fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
1231 val thy = Proof_Context.theory_of ctxt
1232 fun aux arity (CombApp (tm1, tm2)) =
1233 CombApp (aux (arity + 1) tm1, aux 0 tm2)
1234 | aux arity (CombConst (name as (s, _), T, T_args)) =
1235 (case strip_prefix_and_unascii const_prefix s of
1236 NONE => (name, T_args)
1239 val s'' = invert_const s''
1240 fun filtered_T_args false = T_args
1241 | filtered_T_args true = filter_type_args thy s'' arity T_args
1243 case type_arg_policy type_sys s'' of
1244 Explicit_Type_Args drop_args =>
1245 (name, filtered_T_args drop_args)
1246 | Mangled_Type_Args drop_args =>
1247 (mangled_const_name format type_sys (filtered_T_args drop_args)
1249 | No_Type_Args => (name, [])
1251 |> (fn (name, T_args) => CombConst (name, T, T_args))
1255 fun repair_combterm ctxt format type_sys sym_tab =
1256 not (is_setting_higher_order format type_sys)
1257 ? (introduce_explicit_apps_in_combterm sym_tab
1258 #> introduce_predicators_in_combterm sym_tab)
1259 #> enforce_type_arg_policy_in_combterm ctxt format type_sys
1260 fun repair_fact ctxt format type_sys sym_tab =
1261 update_combformula (formula_map
1262 (repair_combterm ctxt format type_sys sym_tab))
1264 (** Helper facts **)
1266 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1268 [(("COMBI", false), @{thms Meson.COMBI_def}),
1269 (("COMBK", false), @{thms Meson.COMBK_def}),
1270 (("COMBB", false), @{thms Meson.COMBB_def}),
1271 (("COMBC", false), @{thms Meson.COMBC_def}),
1272 (("COMBS", false), @{thms Meson.COMBS_def}),
1274 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1275 However, this is done so for backward compatibility: Including the
1276 equality helpers by default in Metis breaks a few existing proofs. *)
1277 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1278 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1279 (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
1280 (("fFalse", true), @{thms True_or_False}),
1281 (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
1282 (("fTrue", true), @{thms True_or_False}),
1284 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1285 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1287 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1288 by (unfold fconj_def) fast+}),
1290 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1291 by (unfold fdisj_def) fast+}),
1292 (("fimplies", false),
1293 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1294 by (unfold fimplies_def) fast+}),
1295 (("If", true), @{thms if_True if_False True_or_False})]
1296 |> map (apsnd (map zero_var_indexes))
1298 val type_tag = `make_fixed_const type_tag_name
1300 fun type_tag_idempotence_fact () =
1302 fun var s = ATerm (`I s, [])
1303 fun tag tm = ATerm (type_tag, [var "T", tm])
1304 val tagged_a = tag (var "A")
1306 Formula (type_tag_idempotence_helper_name, Axiom,
1307 AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
1308 |> close_formula_universally, simp_info, NONE)
1311 fun should_specialize_helper type_sys t =
1312 case general_type_arg_policy type_sys of
1313 Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
1316 fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
1317 case strip_prefix_and_unascii const_prefix s of
1320 val thy = Proof_Context.theory_of ctxt
1321 val unmangled_s = mangled_s |> unmangled_const_name
1322 fun dub_and_inst needs_fairly_sound (th, j) =
1323 ((unmangled_s ^ "_" ^ string_of_int j ^
1324 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1325 (if needs_fairly_sound then typed_helper_suffix
1326 else untyped_helper_suffix),
1328 let val t = th |> prop_of in
1329 t |> should_specialize_helper type_sys t
1331 [T] => specialize_type thy (invert_const unmangled_s, T)
1335 map_filter (make_fact ctxt format type_sys false false false false)
1336 val fairly_sound = is_type_sys_fairly_sound type_sys
1339 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1340 if helper_s <> unmangled_s orelse
1341 (needs_fairly_sound andalso not fairly_sound) then
1344 ths ~~ (1 upto length ths)
1345 |> map (dub_and_inst needs_fairly_sound)
1349 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
1350 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
1353 fun translate_atp_fact ctxt format type_sys keep_trivial =
1354 `(make_fact ctxt format type_sys keep_trivial true true true o apsnd prop_of)
1356 (***************************************************************)
1357 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1358 (***************************************************************)
1360 fun set_insert (x, s) = Symtab.update (x, ()) s
1362 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1364 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1365 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1367 fun classes_of_terms get_Ts =
1368 map (map snd o get_Ts)
1369 #> List.foldl add_classes Symtab.empty
1370 #> delete_type #> Symtab.keys
1372 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
1373 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
1375 (*fold type constructors*)
1376 fun fold_type_constrs f (Type (a, Ts)) x =
1377 fold (fold_type_constrs f) Ts (f (a,x))
1378 | fold_type_constrs _ _ x = x
1380 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
1381 fun add_type_constrs_in_term thy =
1383 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1384 | add (t $ u) = add t #> add u
1385 | add (Const (x as (s, _))) =
1386 if String.isPrefix skolem_const_prefix s then I
1387 else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
1388 | add (Abs (_, _, u)) = add u
1392 fun type_constrs_of_terms thy ts =
1393 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1395 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
1398 val thy = Proof_Context.theory_of ctxt
1399 val fact_ts = map (prop_of o snd o snd) rich_facts
1400 val (facts, fact_names) =
1402 |> map_filter (fn (NONE, _) => NONE
1403 | (SOME fact, (name, _)) => SOME (fact, name))
1405 (* Remove existing facts from the conjecture, as this can dramatically
1406 boost an ATP's performance (for some reason). *)
1409 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1410 val goal_t = Logic.list_implies (hyp_ts, concl_t)
1411 val all_ts = goal_t :: fact_ts
1412 val subs = tfree_classes_of_terms all_ts
1413 val supers = tvar_classes_of_terms all_ts
1414 val tycons = type_constrs_of_terms thy all_ts
1417 |> make_conjecture ctxt format prem_kind type_sys preproc
1418 val (supers', arity_clauses) =
1419 if level_of_type_sys type_sys = No_Types then ([], [])
1420 else make_arity_clauses thy tycons supers
1421 val class_rel_clauses = make_class_rel_clauses thy subs supers'
1423 (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
1426 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
1427 (true, ATerm (class, [ATerm (name, [])]))
1428 | fo_literal_from_type_literal (TyLitFree (class, name)) =
1429 (true, ATerm (class, [ATerm (name, [])]))
1431 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
1433 val type_pred = `make_fixed_const type_pred_name
1435 fun type_pred_combterm ctxt format type_sys T tm =
1436 CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
1437 |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
1439 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
1440 | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1441 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1442 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
1443 | is_var_nonmonotonic_in_formula pos phi _ name =
1444 formula_fold pos (var_occurs_positively_naked_in_term name) phi false
1446 fun mk_const_aterm format type_sys x T_args args =
1447 ATerm (x, map (fo_term_from_typ format type_sys) T_args @ args)
1449 fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
1450 CombConst (type_tag, T --> T, [T])
1451 |> enforce_type_arg_policy_in_combterm ctxt format type_sys
1452 |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
1453 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
1454 and term_from_combterm ctxt format nonmono_Ts type_sys =
1458 val (head, args) = strip_combterm_comb u
1459 val (x as (s, _), T_args) =
1461 CombConst (name, _, T_args) => (name, T_args)
1462 | CombVar (name, _) => (name, [])
1463 | CombApp _ => raise Fail "impossible \"CombApp\""
1464 val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg
1466 val t = mk_const_aterm format type_sys x T_args
1467 (map (aux arg_site) args)
1468 val T = combtyp_of u
1470 t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
1471 tag_with_type ctxt format nonmono_Ts type_sys T
1476 and formula_from_combformula ctxt format nonmono_Ts type_sys
1477 should_predicate_on_var =
1479 val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
1482 Simple_Types level =>
1483 homogenized_type ctxt nonmono_Ts level 0
1484 #> mangled_type format type_sys false 0 #> SOME
1486 fun do_out_of_bound_type pos phi universal (name, T) =
1487 if should_predicate_on_type ctxt nonmono_Ts type_sys
1488 (fn () => should_predicate_on_var pos phi universal name) T then
1490 |> type_pred_combterm ctxt format type_sys T
1491 |> do_term |> AAtom |> SOME
1494 fun do_formula pos (AQuant (q, xs, phi)) =
1496 val phi = phi |> do_formula pos
1497 val universal = Option.map (q = AExists ? not) pos
1499 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1500 | SOME T => do_bound_type T)),
1501 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1503 (fn (_, NONE) => NONE
1505 do_out_of_bound_type pos phi universal (s, T))
1509 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1510 | do_formula _ (AAtom tm) = AAtom (do_term tm)
1511 in do_formula o SOME end
1513 fun bound_tvars type_sys Ts =
1514 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
1515 (type_literals_for_types type_sys sorts_on_tvar Ts))
1517 fun formula_for_fact ctxt format nonmono_Ts type_sys
1518 ({combformula, atomic_types, ...} : translated_formula) =
1520 |> close_combformula_universally
1521 |> formula_from_combformula ctxt format nonmono_Ts type_sys
1522 is_var_nonmonotonic_in_formula true
1523 |> bound_tvars type_sys atomic_types
1524 |> close_formula_universally
1526 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1527 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1528 the remote provers might care. *)
1529 fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
1530 (j, formula as {name, locality, kind, ...}) =
1533 polymorphism_of_type_sys type_sys <> Polymorphic then
1534 string_of_int j ^ "_"
1537 kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
1544 fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
1545 : class_rel_clause) =
1546 let val ty_arg = ATerm (`I "T", []) in
1547 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1548 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
1549 AAtom (ATerm (superclass, [ty_arg]))])
1550 |> close_formula_universally, intro_info, NONE)
1553 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
1554 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
1555 | fo_literal_from_arity_literal (TVarLit (c, sort)) =
1556 (false, ATerm (c, [ATerm (sort, [])]))
1558 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
1560 Formula (arity_clause_prefix ^ ascii_of name, Axiom,
1561 mk_ahorn (map (formula_from_fo_literal o apfst not
1562 o fo_literal_from_arity_literal) prem_lits)
1563 (formula_from_fo_literal
1564 (fo_literal_from_arity_literal concl_lits))
1565 |> close_formula_universally, intro_info, NONE)
1567 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
1568 ({name, kind, combformula, atomic_types, ...} : translated_formula) =
1569 Formula (conjecture_prefix ^ name, kind,
1570 formula_from_combformula ctxt format nonmono_Ts type_sys
1571 is_var_nonmonotonic_in_formula false
1572 (close_combformula_universally combformula)
1573 |> bound_tvars type_sys atomic_types
1574 |> close_formula_universally, NONE, NONE)
1576 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
1577 atomic_types |> type_literals_for_types type_sys sorts_on_tfree
1578 |> map fo_literal_from_type_literal
1580 fun formula_line_for_free_type j lit =
1581 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
1582 formula_from_fo_literal lit, NONE, NONE)
1583 fun formula_lines_for_free_types type_sys facts =
1585 val litss = map (free_type_literals type_sys) facts
1586 val lits = fold (union (op =)) litss []
1587 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
1589 (** Symbol declarations **)
1591 fun should_declare_sym type_sys pred_sym s =
1592 is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
1594 Simple_Types _ => true
1595 | Tags (_, _, Lightweight) => true
1596 | _ => not pred_sym)
1598 fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
1600 fun add_combterm in_conj tm =
1601 let val (head, args) = strip_combterm_comb tm in
1603 CombConst ((s, s'), T, T_args) =>
1604 let val pred_sym = is_pred_sym repaired_sym_tab s in
1605 if should_declare_sym type_sys pred_sym s then
1606 Symtab.map_default (s, [])
1607 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
1613 #> fold (add_combterm in_conj) args
1615 fun add_fact in_conj =
1616 fact_lift (formula_fold NONE (K (add_combterm in_conj)))
1619 |> is_type_sys_fairly_sound type_sys
1620 ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
1623 (* These types witness that the type classes they belong to allow infinite
1624 models and hence that any types with these type classes is monotonic. *)
1625 val known_infinite_types =
1626 [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
1628 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
1629 out with monotonicity" paper presented at CADE 2011. *)
1630 fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
1631 | add_combterm_nonmonotonic_types ctxt level _
1632 (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
1634 (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
1636 Nonmonotonic_Types =>
1637 not (is_type_surely_infinite ctxt known_infinite_types T)
1638 | Finite_Types => is_type_surely_finite ctxt T
1639 | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
1640 | add_combterm_nonmonotonic_types _ _ _ _ = I
1641 fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}
1642 : translated_formula) =
1643 formula_fold (SOME (kind <> Conjecture))
1644 (add_combterm_nonmonotonic_types ctxt level) combformula
1645 fun nonmonotonic_types_for_facts ctxt type_sys facts =
1646 let val level = level_of_type_sys type_sys in
1647 if level = Nonmonotonic_Types orelse level = Finite_Types then
1648 [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
1649 (* We must add "bool" in case the helper "True_or_False" is added
1650 later. In addition, several places in the code rely on the list of
1651 nonmonotonic types not being empty. *)
1652 |> insert_type ctxt I @{typ bool}
1657 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
1658 (s', T_args, T, pred_sym, ary, _) =
1660 val (T_arg_Ts, level) =
1662 Simple_Types level => ([], level)
1663 | _ => (replicate (length T_args) homo_infinite_type, No_Types)
1665 Decl (sym_decl_prefix ^ s, (s, s'),
1666 (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
1667 |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
1670 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
1672 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
1673 type_sys n s j (s', T_args, T, _, ary, in_conj) =
1675 val (kind, maybe_negate) =
1676 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1678 val (arg_Ts, res_T) = chop_fun ary T
1680 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
1682 bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
1684 arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
1687 Formula (preds_sym_formula_prefix ^ s ^
1688 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1689 CombConst ((s, s'), T, T_args)
1690 |> fold (curry (CombApp o swap)) bounds
1691 |> type_pred_combterm ctxt format type_sys res_T
1692 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1693 |> formula_from_combformula ctxt format nonmono_Ts type_sys
1694 (K (K (K (K true)))) true
1695 |> n > 1 ? bound_tvars type_sys (atyps_of T)
1696 |> close_formula_universally
1701 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
1702 nonmono_Ts type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
1705 lightweight_tags_sym_formula_prefix ^ s ^
1706 (if n > 1 then "_" ^ string_of_int j else "")
1707 val (kind, maybe_negate) =
1708 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1710 val (arg_Ts, res_T) = chop_fun ary T
1712 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
1713 val bounds = bound_names |> map (fn name => ATerm (name, []))
1714 val cst = mk_const_aterm format type_sys (s, s') T_args
1715 val atomic_Ts = atyps_of T
1717 (if pred_sym then AConn (AIff, map AAtom tms)
1718 else AAtom (ATerm (`I tptp_equal, tms)))
1719 |> bound_tvars type_sys atomic_Ts
1720 |> close_formula_universally
1722 val should_encode = should_encode_type ctxt nonmono_Ts All_Types
1723 val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
1724 val add_formula_for_res =
1725 if should_encode res_T then
1726 cons (Formula (ident_base ^ "_res", kind,
1727 eq [tag_with res_T (cst bounds), cst bounds],
1731 fun add_formula_for_arg k =
1732 let val arg_T = nth arg_Ts k in
1733 if should_encode arg_T then
1734 case chop k bounds of
1735 (bounds1, bound :: bounds2) =>
1736 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
1737 eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
1740 | _ => raise Fail "expected nonempty tail"
1745 [] |> not pred_sym ? add_formula_for_res
1746 |> fold add_formula_for_arg (ary - 1 downto 0)
1749 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
1751 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
1755 decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
1760 decl :: (decls' as _ :: _) =>
1761 let val T = result_type_of_decl decl in
1762 if forall (curry (type_instance ctxt o swap) T
1763 o result_type_of_decl) decls' then
1769 val n = length decls
1772 |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
1773 o result_type_of_decl)
1775 (0 upto length decls - 1, decls)
1776 |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
1777 nonmono_Ts type_sys n s)
1779 | Tags (_, _, heaviness) =>
1783 let val n = length decls in
1784 (0 upto n - 1 ~~ decls)
1785 |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
1786 conj_sym_kind nonmono_Ts type_sys n s)
1789 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1790 type_sys sym_decl_tab =
1795 |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
1796 nonmono_Ts type_sys)
1798 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
1799 poly <> Mangled_Monomorphic andalso
1800 ((level = All_Types andalso heaviness = Lightweight) orelse
1801 level = Nonmonotonic_Types orelse level = Finite_Types)
1802 | needs_type_tag_idempotence _ = false
1804 fun offset_of_heading_in_problem _ [] j = j
1805 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
1806 if heading = needle then j
1807 else offset_of_heading_in_problem needle problem (j + length lines)
1809 val implicit_declsN = "Should-be-implicit typings"
1810 val explicit_declsN = "Explicit typings"
1811 val factsN = "Relevant facts"
1812 val class_relsN = "Class relationships"
1813 val aritiesN = "Arities"
1814 val helpersN = "Helper facts"
1815 val conjsN = "Conjectures"
1816 val free_typesN = "Type variables"
1818 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
1819 explicit_apply readable_names preproc hyp_ts concl_t
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 lavish_nonmono_Ts =
1836 if null nonmono_Ts 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
1845 lavish_nonmono_Ts type_sys
1847 0 upto length helpers - 1 ~~ helpers
1848 |> map (formula_line_for_fact ctxt format helper_prefix I false
1849 lavish_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 true
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)