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 Metis and Sledgehammer.
9 signature ATP_TRANSLATE =
11 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
12 type connective = ATP_Problem.connective
13 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
14 type format = ATP_Problem.format
15 type formula_kind = ATP_Problem.formula_kind
16 type 'a problem = 'a ATP_Problem.problem
19 General | Helper | Induction | Extensionality | Intro | Elim | Simp |
20 Local | Assum | Chained
22 datatype order = First_Order | Higher_Order
23 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
24 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
27 Noninf_Nonmono_Types of soundness |
31 datatype type_uniformity = Uniform | Nonuniform
34 Simple_Types of order * polymorphism * type_level |
35 Guards of polymorphism * type_level * type_uniformity |
36 Tags of polymorphism * type_level * type_uniformity
38 val type_tag_idempotence : bool Config.T
39 val type_tag_arguments : bool Config.T
40 val no_lambdasN : string
41 val concealedN : string
43 val combinatorsN : string
47 val schematic_var_prefix : string
48 val fixed_var_prefix : string
49 val tvar_prefix : string
50 val tfree_prefix : string
51 val const_prefix : string
52 val type_const_prefix : string
53 val class_prefix : string
54 val polymorphic_free_prefix : string
55 val skolem_const_prefix : string
56 val old_skolem_const_prefix : string
57 val new_skolem_const_prefix : string
58 val type_decl_prefix : string
59 val sym_decl_prefix : string
60 val guards_sym_formula_prefix : string
61 val tags_sym_formula_prefix : string
62 val fact_prefix : string
63 val conjecture_prefix : string
64 val helper_prefix : string
65 val class_rel_clause_prefix : string
66 val arity_clause_prefix : string
67 val tfree_clause_prefix : string
68 val typed_helper_suffix : string
69 val untyped_helper_suffix : string
70 val type_tag_idempotence_helper_name : string
71 val predicator_name : string
72 val app_op_name : string
73 val type_guard_name : string
74 val type_tag_name : string
75 val simple_type_prefix : string
76 val prefixed_predicator_name : string
77 val prefixed_app_op_name : string
78 val prefixed_type_tag_name : string
79 val ascii_of : string -> string
80 val unascii_of : string -> string
81 val strip_prefix_and_unascii : string -> string -> string option
82 val proxy_table : (string * (string * (thm * (string * string)))) list
83 val proxify_const : string -> (string * string) option
84 val invert_const : string -> string
85 val unproxify_const : string -> string
86 val new_skolem_var_name_from_const : string -> string
87 val atp_irrelevant_consts : string list
88 val atp_schematic_consts_of : term -> typ list Symtab.table
89 val type_enc_from_string : soundness -> string -> type_enc
90 val is_type_enc_higher_order : type_enc -> bool
91 val polymorphism_of_type_enc : type_enc -> polymorphism
92 val level_of_type_enc : type_enc -> type_level
93 val is_type_enc_quasi_sound : type_enc -> bool
94 val is_type_enc_fairly_sound : type_enc -> bool
95 val adjust_type_enc : format -> type_enc -> type_enc
97 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
98 val unmangled_const : string -> string * (string, 'b) ho_term list
99 val unmangled_const_name : string -> string
100 val helper_table : ((string * bool) * thm list) list
102 val prepare_atp_problem :
103 Proof.context -> format -> formula_kind -> formula_kind -> type_enc
104 -> bool -> string -> bool -> bool -> term list -> term
105 -> ((string * locality) * term) list
106 -> string problem * string Symtab.table * int * int
107 * (string * locality) list vector * int list * int Symtab.table
108 val atp_problem_weights : string problem -> (string * real) list
111 structure ATP_Translate : ATP_TRANSLATE =
117 type name = string * string
119 val type_tag_idempotence =
120 Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
121 val type_tag_arguments =
122 Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
124 val no_lambdasN = "no_lambdas"
125 val concealedN = "concealed"
126 val liftingN = "lifting"
127 val combinatorsN = "combinators"
128 val hybridN = "hybrid"
129 val lambdasN = "lambdas"
132 val generate_info = false (* experimental *)
134 fun isabelle_info s =
135 if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
142 (* TFF1 is still in development, and it is still unclear whether symbols will be
143 allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
144 "dummy" type variables. *)
145 val exploit_tff1_dummy_type_vars = false
147 val bound_var_prefix = "B_"
148 val all_bound_var_prefix = "BA_"
149 val exist_bound_var_prefix = "BE_"
150 val schematic_var_prefix = "V_"
151 val fixed_var_prefix = "v_"
152 val tvar_prefix = "T_"
153 val tfree_prefix = "t_"
154 val const_prefix = "c_"
155 val type_const_prefix = "tc_"
156 val simple_type_prefix = "s_"
157 val class_prefix = "cl_"
159 val polymorphic_free_prefix = "poly_free"
161 val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
162 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
163 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
165 val type_decl_prefix = "ty_"
166 val sym_decl_prefix = "sy_"
167 val guards_sym_formula_prefix = "gsy_"
168 val tags_sym_formula_prefix = "tsy_"
169 val fact_prefix = "fact_"
170 val conjecture_prefix = "conj_"
171 val helper_prefix = "help_"
172 val class_rel_clause_prefix = "clar_"
173 val arity_clause_prefix = "arity_"
174 val tfree_clause_prefix = "tfree_"
176 val lambda_fact_prefix = "ATP.lambda_"
177 val typed_helper_suffix = "_T"
178 val untyped_helper_suffix = "_U"
179 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
181 val predicator_name = "pp"
182 val app_op_name = "aa"
183 val type_guard_name = "gg"
184 val type_tag_name = "tt"
186 val prefixed_predicator_name = const_prefix ^ predicator_name
187 val prefixed_app_op_name = const_prefix ^ app_op_name
188 val prefixed_type_tag_name = const_prefix ^ type_tag_name
190 (* Freshness almost guaranteed! *)
191 val atp_weak_prefix = "ATP:"
193 (*Escaping of special characters.
194 Alphanumeric characters are left unchanged.
195 The character _ goes to __
196 Characters in the range ASCII space to / go to _A to _P, respectively.
197 Other characters go to _nnn where nnn is the decimal ASCII code.*)
198 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
200 fun stringN_of_int 0 _ = ""
201 | stringN_of_int k n =
202 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
204 fun ascii_of_char c =
205 if Char.isAlphaNum c then
207 else if c = #"_" then
209 else if #" " <= c andalso c <= #"/" then
210 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
212 (* fixed width, in case more digits follow *)
213 "_" ^ stringN_of_int 3 (Char.ord c)
215 val ascii_of = String.translate ascii_of_char
217 (** Remove ASCII armoring from names in proof files **)
219 (* We don't raise error exceptions because this code can run inside a worker
220 thread. Also, the errors are impossible. *)
223 fun un rcs [] = String.implode(rev rcs)
224 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
225 (* Three types of _ escapes: __, _A to _P, _nnn *)
226 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
227 | un rcs (#"_" :: c :: cs) =
228 if #"A" <= c andalso c<= #"P" then
229 (* translation of #" " to #"/" *)
230 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
232 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
233 case Int.fromString (String.implode digits) of
234 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
235 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
237 | un rcs (c :: cs) = un (c :: rcs) cs
238 in un [] o String.explode end
240 (* If string s has the prefix s1, return the result of deleting it,
242 fun strip_prefix_and_unascii s1 s =
243 if String.isPrefix s1 s then
244 SOME (unascii_of (String.extract (s, size s1, NONE)))
249 [("c_False", (@{const_name False}, (@{thm fFalse_def},
250 ("fFalse", @{const_name ATP.fFalse})))),
251 ("c_True", (@{const_name True}, (@{thm fTrue_def},
252 ("fTrue", @{const_name ATP.fTrue})))),
253 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
254 ("fNot", @{const_name ATP.fNot})))),
255 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
256 ("fconj", @{const_name ATP.fconj})))),
257 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
258 ("fdisj", @{const_name ATP.fdisj})))),
259 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
260 ("fimplies", @{const_name ATP.fimplies})))),
261 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
262 ("fequal", @{const_name ATP.fequal})))),
263 ("c_All", (@{const_name All}, (@{thm fAll_def},
264 ("fAll", @{const_name ATP.fAll})))),
265 ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
266 ("fEx", @{const_name ATP.fEx}))))]
268 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
270 (* Readable names for the more common symbolic functions. Do not mess with the
271 table unless you know what you are doing. *)
272 val const_trans_table =
273 [(@{type_name Product_Type.prod}, "prod"),
274 (@{type_name Sum_Type.sum}, "sum"),
275 (@{const_name False}, "False"),
276 (@{const_name True}, "True"),
277 (@{const_name Not}, "Not"),
278 (@{const_name conj}, "conj"),
279 (@{const_name disj}, "disj"),
280 (@{const_name implies}, "implies"),
281 (@{const_name HOL.eq}, "equal"),
282 (@{const_name All}, "All"),
283 (@{const_name Ex}, "Ex"),
284 (@{const_name If}, "If"),
285 (@{const_name Set.member}, "member"),
286 (@{const_name Meson.COMBI}, "COMBI"),
287 (@{const_name Meson.COMBK}, "COMBK"),
288 (@{const_name Meson.COMBB}, "COMBB"),
289 (@{const_name Meson.COMBC}, "COMBC"),
290 (@{const_name Meson.COMBS}, "COMBS")]
292 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
294 (* Invert the table of translations between Isabelle and ATPs. *)
295 val const_trans_table_inv =
296 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
297 val const_trans_table_unprox =
299 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
301 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
302 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
305 case Symtab.lookup const_trans_table c of
309 fun ascii_of_indexname (v, 0) = ascii_of v
310 | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
312 fun make_bound_var x = bound_var_prefix ^ ascii_of x
313 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
314 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
315 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
316 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
318 fun make_schematic_type_var (x, i) =
319 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
320 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
322 (* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
324 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
325 fun default c = const_prefix ^ lookup_const c
327 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
328 | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
329 if c = choice_const then tptp_choice else default c
330 | make_fixed_const _ c = default c
333 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
335 fun make_type_class clas = class_prefix ^ ascii_of clas
337 fun new_skolem_var_name_from_const s =
338 let val ss = s |> space_explode Long_Name.separator in
339 nth ss (length ss - 2)
342 (* These are either simplified away by "Meson.presimplify" (most of the time) or
343 handled specially via "fFalse", "fTrue", ..., "fequal". *)
344 val atp_irrelevant_consts =
345 [@{const_name False}, @{const_name True}, @{const_name Not},
346 @{const_name conj}, @{const_name disj}, @{const_name implies},
347 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
349 val atp_monomorph_bad_consts =
350 atp_irrelevant_consts @
351 (* These are ignored anyway by the relevance filter (unless they appear in
352 higher-order places) but not by the monomorphizer. *)
353 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
354 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
355 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
357 fun add_schematic_const (x as (_, T)) =
358 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
359 val add_schematic_consts_of =
360 Term.fold_aterms (fn Const (x as (s, _)) =>
361 not (member (op =) atp_monomorph_bad_consts s)
362 ? add_schematic_const x
364 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
366 (** Definitions and functions for FOL clauses and formulas for TPTP **)
368 (* The first component is the type class; the second is a "TVar" or "TFree". *)
369 datatype type_literal =
370 TyLitVar of name * name |
371 TyLitFree of name * name
374 (** Isabelle arities **)
376 datatype arity_literal =
377 AryLitConst of name * name * name list |
378 AryLitVar of name * name
380 val type_class = the_single @{sort type}
382 fun add_packed_sort tvar =
383 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
387 prem_lits : arity_literal list,
388 concl_lits : arity_literal}
390 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
391 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
393 val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
394 val tvars_srts = ListPair.zip (tvars, args)
398 [] |> fold (uncurry add_packed_sort) tvars_srts |> map AryLitVar,
400 AryLitConst (`make_type_class cls, `make_fixed_type_const tcons,
404 fun arity_clause _ _ (_, []) = []
405 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
406 arity_clause seen n (tcons, ars)
407 | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
408 if member (op =) seen class then
409 (* multiple arities for the same (tycon, class) pair *)
410 make_axiom_arity_clause (tcons,
411 lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
413 arity_clause seen (n + 1) (tcons, ars)
415 make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
416 ascii_of class, ar) ::
417 arity_clause (class :: seen) n (tcons, ars)
419 fun multi_arity_clause [] = []
420 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
421 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
423 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
424 theory thy provided its arguments have the corresponding sorts. *)
425 fun type_class_pairs thy tycons classes =
427 val alg = Sign.classes_of thy
428 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
429 fun add_class tycon class =
430 cons (class, domain_sorts tycon class)
431 handle Sorts.CLASS_ERROR _ => I
432 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
433 in map try_classes tycons end
435 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
436 fun iter_type_class_pairs _ _ [] = ([], [])
437 | iter_type_class_pairs thy tycons classes =
439 fun maybe_insert_class s =
440 (s <> type_class andalso not (member (op =) classes s))
442 val cpairs = type_class_pairs thy tycons classes
444 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
445 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
446 in (classes' @ classes, union (op =) cpairs' cpairs) end
448 fun make_arity_clauses thy tycons =
449 iter_type_class_pairs thy tycons ##> multi_arity_clause
452 (** Isabelle class relations **)
454 type class_rel_clause =
459 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
461 fun class_pairs _ [] _ = []
462 | class_pairs thy subs supers =
464 val class_less = Sorts.class_less (Sign.classes_of thy)
465 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
466 fun add_supers sub = fold (add_super sub) supers
467 in fold add_supers subs [] end
469 fun make_class_rel_clause (sub, super) =
470 {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
471 superclass = `make_type_class super}
473 fun make_class_rel_clauses thy subs supers =
474 map make_class_rel_clause (class_pairs thy subs supers)
476 (* intermediate terms *)
478 IConst of name * typ * typ list |
480 IApp of iterm * iterm |
481 IAbs of (name * typ) * iterm
483 fun ityp_of (IConst (_, T, _)) = T
484 | ityp_of (IVar (_, T)) = T
485 | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
486 | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
488 (*gets the head of a combinator application, along with the list of arguments*)
489 fun strip_iterm_comb u =
491 fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
493 in stripc (u, []) end
495 fun atyps_of T = fold_atyps (insert (op =)) T []
497 fun new_skolem_const_name s num_T_args =
498 [new_skolem_const_prefix, s, string_of_int num_T_args]
499 |> space_implode Long_Name.separator
501 fun robust_const_type thy s =
502 if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
503 else s |> Sign.the_const_type thy
505 (* This function only makes sense if "T" is as general as possible. *)
506 fun robust_const_typargs thy (s, T) =
507 (s, T) |> Sign.const_typargs thy
508 handle TYPE _ => [] |> Term.add_tvarsT T |> rev |> map TVar
510 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
511 Also accumulates sort infomation. *)
512 fun iterm_from_term thy format bs (P $ Q) =
514 val (P', P_atomics_Ts) = iterm_from_term thy format bs P
515 val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
516 in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
517 | iterm_from_term thy format _ (Const (c, T)) =
518 (IConst (`(make_fixed_const (SOME format)) c, T,
519 robust_const_typargs thy (c, T)),
521 | iterm_from_term _ _ _ (Free (s, T)) =
522 (IConst (`make_fixed_var s, T,
523 if String.isPrefix polymorphic_free_prefix s then [T] else []),
525 | iterm_from_term _ format _ (Var (v as (s, _), T)) =
526 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
528 val Ts = T |> strip_type |> swap |> op ::
529 val s' = new_skolem_const_name s (length Ts)
530 in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
532 IVar ((make_schematic_var v, s), T), atyps_of T)
533 | iterm_from_term _ _ bs (Bound j) =
534 nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T))
535 | iterm_from_term thy format bs (Abs (s, T, t)) =
537 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
539 val name = `make_bound_var s
540 val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
541 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
544 General | Helper | Induction | Extensionality | Intro | Elim | Simp |
545 Local | Assum | Chained
547 datatype order = First_Order | Higher_Order
548 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
549 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
550 datatype type_level =
552 Noninf_Nonmono_Types of soundness |
556 datatype type_uniformity = Uniform | Nonuniform
559 Simple_Types of order * polymorphism * type_level |
560 Guards of polymorphism * type_level * type_uniformity |
561 Tags of polymorphism * type_level * type_uniformity
563 fun try_unsuffixes ss s =
564 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
566 fun type_enc_from_string soundness s =
567 (case try (unprefix "poly_") s of
568 SOME s => (SOME Polymorphic, s)
570 case try (unprefix "raw_mono_") s of
571 SOME s => (SOME Raw_Monomorphic, s)
573 case try (unprefix "mono_") s of
574 SOME s => (SOME Mangled_Monomorphic, s)
577 (* "_query" and "_bang" are for the ASCII-challenged Metis and
579 case try_unsuffixes ["?", "_query"] s of
580 SOME s => (Noninf_Nonmono_Types soundness, s)
582 case try_unsuffixes ["!", "_bang"] s of
583 SOME s => (Fin_Nonmono_Types, s)
584 | NONE => (All_Types, s))
586 case try (unsuffix "_uniform") s of
587 SOME s => (Uniform, s)
588 | NONE => (Nonuniform, s))
589 |> (fn (poly, (level, (uniformity, core))) =>
590 case (core, (poly, level, uniformity)) of
591 ("simple", (SOME poly, _, Nonuniform)) =>
593 Raw_Monomorphic => raise Same.SAME
594 | _ => Simple_Types (First_Order, poly, level))
595 | ("simple_higher", (SOME poly, _, Nonuniform)) =>
596 (case (poly, level) of
597 (Raw_Monomorphic, _) => raise Same.SAME
598 | (_, Noninf_Nonmono_Types _) => raise Same.SAME
599 | _ => Simple_Types (Higher_Order, poly, level))
600 | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
601 | ("tags", (SOME Polymorphic, _, _)) =>
602 Tags (Polymorphic, level, uniformity)
603 | ("tags", (SOME poly, _, _)) => Tags (poly, level, uniformity)
604 | ("args", (SOME poly, All_Types (* naja *), Nonuniform)) =>
605 Guards (poly, Const_Arg_Types, Nonuniform)
606 | ("erased", (NONE, All_Types (* naja *), Nonuniform)) =>
607 Guards (Polymorphic, No_Types, Nonuniform)
608 | _ => raise Same.SAME)
609 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
611 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
612 | is_type_enc_higher_order _ = false
614 fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
615 | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
616 | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
618 fun level_of_type_enc (Simple_Types (_, _, level)) = level
619 | level_of_type_enc (Guards (_, level, _)) = level
620 | level_of_type_enc (Tags (_, level, _)) = level
622 fun uniformity_of_type_enc (Simple_Types _) = Uniform
623 | uniformity_of_type_enc (Guards (_, _, uniformity)) = uniformity
624 | uniformity_of_type_enc (Tags (_, _, uniformity)) = uniformity
626 fun is_type_level_quasi_sound All_Types = true
627 | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
628 | is_type_level_quasi_sound _ = false
629 val is_type_enc_quasi_sound =
630 is_type_level_quasi_sound o level_of_type_enc
632 fun is_type_level_fairly_sound level =
633 is_type_level_quasi_sound level orelse level = Fin_Nonmono_Types
634 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
636 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
637 | is_type_level_monotonicity_based Fin_Nonmono_Types = true
638 | is_type_level_monotonicity_based _ = false
640 fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
641 Simple_Types (order, Mangled_Monomorphic, level)
642 | adjust_type_enc (THF0 _) type_enc = type_enc
643 | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
644 Simple_Types (First_Order, Mangled_Monomorphic, level)
645 | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
646 Simple_Types (First_Order, poly, level)
647 | adjust_type_enc format (Simple_Types (_, poly, level)) =
648 adjust_type_enc format (Guards (poly, level, Uniform))
649 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
650 (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
651 | adjust_type_enc _ type_enc = type_enc
653 fun lift_lambdas ctxt type_enc =
654 map (close_form o Envir.eta_contract) #> rpair ctxt
655 #-> Lambda_Lifting.lift_lambdas
656 (if polymorphism_of_type_enc type_enc = Polymorphic then
657 SOME polymorphic_free_prefix
660 Lambda_Lifting.is_quantifier
663 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
665 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
667 fun lam T t = Abs (Name.uu, T, t)
668 val (head, args) = strip_comb t ||> rev
669 val head_T = fastype_of head
671 val arg_Ts = head_T |> binder_types |> take n |> rev
672 val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
673 in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
674 | intentionalize_def t = t
676 type translated_formula =
680 iformula : (name, typ, iterm) formula,
681 atomic_types : typ list}
683 fun update_iformula f ({name, locality, kind, iformula, atomic_types}
684 : translated_formula) =
685 {name = name, locality = locality, kind = kind, iformula = f iformula,
686 atomic_types = atomic_types} : translated_formula
688 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
690 fun insert_type ctxt get_T x xs =
691 let val T = get_T x in
692 if exists (type_instance ctxt T o get_T) xs then xs
693 else x :: filter_out (type_generalization ctxt T o get_T) xs
696 (* The Booleans indicate whether all type arguments should be kept. *)
697 datatype type_arg_policy =
698 Explicit_Type_Args of bool |
699 Mangled_Type_Args of bool |
702 fun should_drop_arg_type_args (Simple_Types _) = false
703 | should_drop_arg_type_args type_enc =
704 level_of_type_enc type_enc = All_Types andalso
705 uniformity_of_type_enc type_enc = Uniform
707 fun type_arg_policy type_enc s =
708 if s = type_tag_name then
709 (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
712 Explicit_Type_Args) false
713 else case type_enc of
714 Tags (_, All_Types, Uniform) => No_Type_Args
716 let val level = level_of_type_enc type_enc in
717 if level = No_Types orelse s = @{const_name HOL.eq} orelse
718 (s = app_op_name andalso level = Const_Arg_Types) then
721 should_drop_arg_type_args type_enc
722 |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
728 (* Make literals for sorted type variables. *)
729 fun generic_add_sorts_on_type (_, []) = I
730 | generic_add_sorts_on_type ((x, i), s :: ss) =
731 generic_add_sorts_on_type ((x, i), ss)
732 #> (if s = the_single @{sort HOL.type} then
735 insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
737 insert (op =) (TyLitVar (`make_type_class s,
738 (make_schematic_type_var (x, i), x))))
739 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
740 | add_sorts_on_tfree _ = I
741 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
742 | add_sorts_on_tvar _ = I
744 fun type_literals_for_types type_enc add_sorts_on_typ Ts =
745 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
747 fun mk_aconns c phis =
748 let val (phis', phi') = split_last phis in
749 fold_rev (mk_aconn c) phis' phi'
751 fun mk_ahorn [] phi = phi
752 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
753 fun mk_aquant _ [] phi = phi
754 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
755 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
756 | mk_aquant q xs phi = AQuant (q, xs, phi)
758 fun close_universally atom_vars phi =
760 fun formula_vars bounds (AQuant (_, xs, phi)) =
761 formula_vars (map fst xs @ bounds) phi
762 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
763 | formula_vars bounds (AAtom tm) =
764 union (op =) (atom_vars tm []
765 |> filter_out (member (op =) bounds o fst))
766 in mk_aquant AForall (formula_vars [] phi []) phi end
768 fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2]
769 | iterm_vars (IConst _) = I
770 | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T)
771 | iterm_vars (IAbs (_, tm)) = iterm_vars tm
772 fun close_iformula_universally phi = close_universally iterm_vars phi
774 fun term_vars type_enc =
776 fun vars bounds (ATerm (name as (s, _), tms)) =
777 (if is_tptp_variable s andalso not (member (op =) bounds name) then
779 Simple_Types (_, Polymorphic, _) =>
780 if String.isPrefix tvar_prefix s then SOME atype_of_types
783 |> pair name |> insert (op =)
786 #> fold (vars bounds) tms
787 | vars bounds (AAbs ((name, _), tm)) = vars (name :: bounds) tm
789 fun close_formula_universally type_enc =
790 close_universally (term_vars type_enc [])
792 val fused_infinite_type_name = @{type_name ind} (* any infinite type *)
793 val fused_infinite_type = Type (fused_infinite_type_name, [])
795 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
797 fun ho_term_from_typ format type_enc =
799 fun term (Type (s, Ts)) =
800 ATerm (case (is_type_enc_higher_order type_enc, s) of
801 (true, @{type_name bool}) => `I tptp_bool_type
802 | (true, @{type_name fun}) => `I tptp_fun_type
803 | _ => if s = fused_infinite_type_name andalso
804 is_format_typed format then
805 `I tptp_individual_type
807 `make_fixed_type_const s,
809 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
810 | term (TVar (x, _)) = ATerm (tvar_name x, [])
813 fun ho_term_for_type_arg format type_enc T =
814 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
816 (* This shouldn't clash with anything else. *)
817 val mangled_type_sep = "\000"
819 fun generic_mangled_type_name f (ATerm (name, [])) = f name
820 | generic_mangled_type_name f (ATerm (name, tys)) =
821 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
823 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
825 fun mangled_type format type_enc =
826 generic_mangled_type_name fst o ho_term_from_typ format type_enc
828 fun make_simple_type s =
829 if s = tptp_bool_type orelse s = tptp_fun_type orelse
830 s = tptp_individual_type then
833 simple_type_prefix ^ ascii_of s
835 fun ho_type_from_ho_term type_enc pred_sym ary =
837 fun to_mangled_atype ty =
838 AType ((make_simple_type (generic_mangled_type_name fst ty),
839 generic_mangled_type_name snd ty), [])
840 fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
841 | to_poly_atype _ = raise Fail "unexpected type abstraction"
843 if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
844 else to_mangled_atype
845 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
846 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
847 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
848 | to_fo _ _ = raise Fail "unexpected type abstraction"
849 fun to_ho (ty as ATerm ((s, _), tys)) =
850 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
851 | to_ho _ = raise Fail "unexpected type abstraction"
852 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
854 fun ho_type_from_typ format type_enc pred_sym ary =
855 ho_type_from_ho_term type_enc pred_sym ary
856 o ho_term_from_typ format type_enc
858 fun mangled_const_name format type_enc T_args (s, s') =
860 val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
861 fun type_suffix f g =
862 fold_rev (curry (op ^) o g o prefix mangled_type_sep
863 o generic_mangled_type_name f) ty_args ""
864 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
866 val parse_mangled_ident =
867 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
869 fun parse_mangled_type x =
871 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
873 and parse_mangled_types x =
874 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
876 fun unmangled_type s =
877 s |> suffix ")" |> raw_explode
878 |> Scan.finite Symbol.stopper
879 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
880 quote s)) parse_mangled_type))
883 val unmangled_const_name = space_explode mangled_type_sep #> hd
884 fun unmangled_const s =
885 let val ss = space_explode mangled_type_sep s in
886 (hd ss, map unmangled_type (tl ss))
889 fun introduce_proxies type_enc =
891 fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
892 | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
894 (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
895 limitation. This works in conjuction with special code in
896 "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
899 IApp (IConst (`I ho_quant, T, []),
901 IApp (IConst (`I "P", p_T, []),
902 IConst (`I "X", x_T, [])))))
903 | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
904 fun intro top_level args (IApp (tm1, tm2)) =
905 IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
906 | intro top_level args (IConst (name as (s, _), T, T_args)) =
907 (case proxify_const s of
909 if top_level orelse is_type_enc_higher_order type_enc then
910 case (top_level, s) of
911 (_, "c_False") => IConst (`I tptp_false, T, [])
912 | (_, "c_True") => IConst (`I tptp_true, T, [])
913 | (false, "c_Not") => IConst (`I tptp_not, T, [])
914 | (false, "c_conj") => IConst (`I tptp_and, T, [])
915 | (false, "c_disj") => IConst (`I tptp_or, T, [])
916 | (false, "c_implies") => IConst (`I tptp_implies, T, [])
917 | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
918 | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
920 if is_tptp_equal s andalso length args = 2 then
921 IConst (`I tptp_equal, T, [])
923 (* Use a proxy even for partially applied THF0 equality,
924 because the LEO-II and Satallax parsers complain about not
925 being able to infer the type of "=". *)
926 IConst (proxy_base |>> prefix const_prefix, T, T_args)
927 | _ => IConst (name, T, [])
929 IConst (proxy_base |>> prefix const_prefix, T, T_args)
930 | NONE => if s = tptp_choice then
931 tweak_ho_quant tptp_choice T args
933 IConst (name, T, T_args))
934 | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
938 fun iformula_from_prop thy format type_enc eq_as_iff =
940 fun do_term bs t atomic_types =
941 iterm_from_term thy format bs (Envir.eta_contract t)
942 |>> (introduce_proxies type_enc #> AAtom)
943 ||> union (op =) atomic_types
944 fun do_quant bs q pos s T t' =
946 val s = singleton (Name.variant_list (map fst bs)) s
947 val universal = Option.map (q = AExists ? not) pos
949 s |> `(case universal of
950 SOME true => make_all_bound_var
951 | SOME false => make_exist_bound_var
952 | NONE => make_bound_var)
954 do_formula ((s, (name, T)) :: bs) pos t'
955 #>> mk_aquant q [(name, SOME T)]
957 and do_conn bs c pos1 t1 pos2 t2 =
958 do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
959 and do_formula bs pos t =
961 @{const Trueprop} $ t1 => do_formula bs pos t1
962 | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
963 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
964 do_quant bs AForall pos s T t'
965 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
966 do_quant bs AExists pos s T t'
967 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
968 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
969 | @{const HOL.implies} $ t1 $ t2 =>
970 do_conn bs AImplies (Option.map not pos) t1 pos t2
971 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
972 if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
976 fun presimplify_term _ [] t = t
977 | presimplify_term ctxt presimp_consts t =
978 t |> exists_Const (member (op =) presimp_consts o fst) t
979 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
980 #> Meson.presimplify ctxt
983 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
984 fun conceal_bounds Ts t =
985 subst_bounds (map (Free o apfst concealed_bound_name)
986 (0 upto length Ts - 1 ~~ Ts), t)
987 fun reveal_bounds Ts =
988 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
989 (0 upto length Ts - 1 ~~ Ts))
991 fun is_fun_equality (@{const_name HOL.eq},
992 Type (_, [Type (@{type_name fun}, _), _])) = true
993 | is_fun_equality _ = false
995 fun extensionalize_term ctxt t =
996 if exists_Const is_fun_equality t then
997 let val thy = Proof_Context.theory_of ctxt in
998 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
999 |> prop_of |> Logic.dest_equals |> snd
1004 fun simple_translate_lambdas do_lambdas ctxt t =
1005 let val thy = Proof_Context.theory_of ctxt in
1006 if Meson.is_fol_term thy t then
1012 @{const Not} $ t1 => @{const Not} $ aux Ts t1
1013 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
1014 t0 $ Abs (s, T, aux (T :: Ts) t')
1015 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1016 aux Ts (t0 $ eta_expand Ts t1 1)
1017 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
1018 t0 $ Abs (s, T, aux (T :: Ts) t')
1019 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1020 aux Ts (t0 $ eta_expand Ts t1 1)
1021 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1022 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1023 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1024 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1026 t0 $ aux Ts t1 $ aux Ts t2
1028 if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1029 else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1030 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1031 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
1034 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
1035 do_cheaply_conceal_lambdas Ts t1
1036 $ do_cheaply_conceal_lambdas Ts t2
1037 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
1038 Free (polymorphic_free_prefix ^ serial_string (),
1039 T --> fastype_of1 (T :: Ts, t))
1040 | do_cheaply_conceal_lambdas _ t = t
1042 fun do_introduce_combinators ctxt Ts t =
1043 let val thy = Proof_Context.theory_of ctxt in
1044 t |> conceal_bounds Ts
1046 |> Meson_Clausify.introduce_combinators_in_cterm
1047 |> prop_of |> Logic.dest_equals |> snd
1050 (* A type variable of sort "{}" will make abstraction fail. *)
1051 handle THM _ => t |> do_cheaply_conceal_lambdas Ts
1052 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
1054 fun preprocess_abstractions_in_terms trans_lambdas facts =
1056 val (facts, lambda_ts) =
1057 facts |> map (snd o snd) |> trans_lambdas
1058 |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
1060 map2 (fn t => fn j =>
1061 ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
1062 lambda_ts (1 upto length lambda_ts)
1063 in (facts, lambda_facts) end
1065 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
1066 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
1069 fun aux (t $ u) = aux t $ aux u
1070 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
1071 | aux (Var ((s, i), T)) =
1072 Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
1074 in t |> exists_subterm is_Var t ? aux end
1076 fun presimp_prop ctxt presimp_consts t =
1078 val thy = Proof_Context.theory_of ctxt
1079 val t = t |> Envir.beta_eta_contract
1080 |> transform_elim_prop
1081 |> Object_Logic.atomize_term thy
1082 val need_trueprop = (fastype_of t = @{typ bool})
1084 t |> need_trueprop ? HOLogic.mk_Trueprop
1085 |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
1086 |> extensionalize_term ctxt
1087 |> presimplify_term ctxt presimp_consts
1088 |> perhaps (try (HOLogic.dest_Trueprop))
1091 (* making fact and conjecture formulas *)
1092 fun make_formula thy format type_enc eq_as_iff name loc kind t =
1094 val (iformula, atomic_types) =
1095 iformula_from_prop thy format type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
1097 {name = name, locality = loc, kind = kind, iformula = iformula,
1098 atomic_types = atomic_types}
1101 fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
1102 let val thy = Proof_Context.theory_of ctxt in
1103 case t |> make_formula thy format type_enc (eq_as_iff andalso format <> CNF)
1105 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1106 if s = tptp_true then NONE else SOME formula
1107 | formula => SOME formula
1110 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
1111 | s_not_trueprop t = s_not t
1113 fun make_conjecture thy format type_enc =
1114 map (fn ((name, loc), (kind, t)) =>
1115 t |> kind = Conjecture ? s_not_trueprop
1116 |> make_formula thy format type_enc (format <> CNF) name loc kind)
1118 (** Finite and infinite type inference **)
1120 type monotonicity_info =
1121 {maybe_finite_Ts : typ list,
1122 surely_finite_Ts : typ list,
1123 maybe_infinite_Ts : typ list,
1124 surely_infinite_Ts : typ list,
1125 maybe_nonmono_Ts : typ list}
1127 (* These types witness that the type classes they belong to allow infinite
1128 models and hence that any types with these type classes is monotonic. *)
1129 val known_infinite_types =
1130 [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
1132 fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
1133 soundness <> Sound andalso
1134 is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T
1136 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1137 dangerous because their "exhaust" properties can easily lead to unsound ATP
1138 proofs. On the other hand, all HOL infinite types can be given the same
1139 models in first-order logic (via Löwenheim-Skolem). *)
1141 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
1142 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
1143 maybe_nonmono_Ts, ...}
1144 (Noninf_Nonmono_Types soundness) T =
1145 exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1146 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
1147 (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
1148 is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
1149 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
1150 maybe_nonmono_Ts, ...}
1151 Fin_Nonmono_Types T =
1152 exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1153 (exists (type_generalization ctxt T) surely_finite_Ts orelse
1154 (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
1155 is_type_surely_finite ctxt T))
1156 | should_encode_type _ _ _ _ = false
1158 fun should_guard_type ctxt mono (Guards (_, level, uniformity)) should_guard_var
1160 (uniformity = Uniform orelse should_guard_var ()) andalso
1161 should_encode_type ctxt mono level T
1162 | should_guard_type _ _ _ _ _ = false
1164 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
1165 String.isPrefix bound_var_prefix s orelse
1166 String.isPrefix all_bound_var_prefix s
1167 | is_maybe_universal_var (IVar _) = true
1168 | is_maybe_universal_var _ = false
1171 Top_Level of bool option |
1172 Eq_Arg of bool option |
1175 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1176 | should_tag_with_type ctxt mono (Tags (_, level, uniformity)) site u T =
1178 Uniform => should_encode_type ctxt mono level T
1180 case (site, is_maybe_universal_var u) of
1181 (Eq_Arg _, true) => should_encode_type ctxt mono level T
1183 | should_tag_with_type _ _ _ _ _ _ = false
1185 fun fused_type ctxt mono level =
1187 val should_encode = should_encode_type ctxt mono level
1188 fun fuse 0 T = if should_encode T then T else fused_infinite_type
1189 | fuse ary (Type (@{type_name fun}, [T1, T2])) =
1190 fuse 0 T1 --> fuse (ary - 1) T2
1191 | fuse _ _ = raise Fail "expected function type"
1194 (** predicators and application operators **)
1197 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
1199 fun add_iterm_syms_to_table ctxt explicit_apply =
1201 fun consider_var_arity const_T var_T max_ary =
1204 if ary = max_ary orelse type_instance ctxt var_T T orelse
1205 type_instance ctxt T var_T then
1208 iter (ary + 1) (range_type T)
1209 in iter 0 const_T end
1210 fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1211 if explicit_apply = NONE andalso
1212 (can dest_funT T orelse T = @{typ bool}) then
1214 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1215 fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
1216 {pred_sym = pred_sym andalso not bool_vars',
1217 min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
1218 max_ary = max_ary, types = types}
1220 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1222 if bool_vars' = bool_vars andalso
1223 pointer_eq (fun_var_Ts', fun_var_Ts) then
1226 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
1230 fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1231 let val (head, args) = strip_iterm_comb tm in
1233 IConst ((s, _), T, _) =>
1234 if String.isPrefix bound_var_prefix s orelse
1235 String.isPrefix all_bound_var_prefix s then
1236 add_universal_var T accum
1237 else if String.isPrefix exist_bound_var_prefix s then
1240 let val ary = length args in
1241 ((bool_vars, fun_var_Ts),
1242 case Symtab.lookup sym_tab s of
1243 SOME {pred_sym, min_ary, max_ary, types} =>
1246 pred_sym andalso top_level andalso not bool_vars
1247 val types' = types |> insert_type ctxt I T
1249 if is_some explicit_apply orelse
1250 pointer_eq (types', types) then
1253 fold (consider_var_arity T) fun_var_Ts min_ary
1255 Symtab.update (s, {pred_sym = pred_sym,
1256 min_ary = Int.min (ary, min_ary),
1257 max_ary = Int.max (ary, max_ary),
1263 val pred_sym = top_level andalso not bool_vars
1265 case explicit_apply of
1268 | NONE => fold (consider_var_arity T) fun_var_Ts ary
1270 Symtab.update_new (s, {pred_sym = pred_sym,
1271 min_ary = min_ary, max_ary = ary,
1276 | IVar (_, T) => add_universal_var T accum
1277 | IAbs ((_, T), tm) => accum |> add_universal_var T |> add false tm
1279 |> fold (add false) args
1282 fun add_fact_syms_to_table ctxt explicit_apply =
1283 K (add_iterm_syms_to_table ctxt explicit_apply)
1284 |> formula_fold NONE |> fact_lift
1286 val tvar_a_str = "'a"
1287 val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
1288 val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
1289 val itself_name = `make_fixed_type_const @{type_name itself}
1290 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
1291 val tvar_a_atype = AType (tvar_a_name, [])
1292 val a_itself_atype = AType (itself_name, [tvar_a_atype])
1294 val default_sym_tab_entries : (string * sym_info) list =
1295 (prefixed_predicator_name,
1296 {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
1297 (* FIXME: needed? *) ::
1298 (make_fixed_const NONE @{const_name undefined},
1299 {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
1300 ([tptp_false, tptp_true]
1301 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
1302 ([tptp_equal, tptp_old_equal]
1303 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
1305 fun sym_table_for_facts ctxt explicit_apply facts =
1306 ((false, []), Symtab.empty)
1307 |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
1308 |> fold Symtab.update default_sym_tab_entries
1310 fun min_arity_of sym_tab s =
1311 case Symtab.lookup sym_tab s of
1312 SOME ({min_ary, ...} : sym_info) => min_ary
1314 case strip_prefix_and_unascii const_prefix s of
1316 let val s = s |> unmangled_const_name |> invert_const in
1317 if s = predicator_name then 1
1318 else if s = app_op_name then 2
1319 else if s = type_guard_name then 1
1324 (* True if the constant ever appears outside of the top-level position in
1325 literals, or if it appears with different arities (e.g., because of different
1326 type instantiations). If false, the constant always receives all of its
1327 arguments and is used as a predicate. *)
1328 fun is_pred_sym sym_tab s =
1329 case Symtab.lookup sym_tab s of
1330 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1331 pred_sym andalso min_ary = max_ary
1334 val predicator_combconst =
1335 IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
1336 fun predicator tm = IApp (predicator_combconst, tm)
1338 fun introduce_predicators_in_iterm sym_tab tm =
1339 case strip_iterm_comb tm of
1340 (IConst ((s, _), _, _), _) =>
1341 if is_pred_sym sym_tab s then tm else predicator tm
1342 | _ => predicator tm
1344 fun list_app head args = fold (curry (IApp o swap)) args head
1346 val app_op = `(make_fixed_const NONE) app_op_name
1348 fun explicit_app arg head =
1350 val head_T = ityp_of head
1351 val (arg_T, res_T) = dest_funT head_T
1352 val explicit_app = IConst (app_op, head_T --> head_T, [arg_T, res_T])
1353 in list_app explicit_app [head, arg] end
1354 fun list_explicit_app head args = fold explicit_app args head
1356 fun introduce_explicit_apps_in_iterm sym_tab =
1359 case strip_iterm_comb tm of
1360 (head as IConst ((s, _), _, _), args) =>
1362 |> chop (min_arity_of sym_tab s)
1364 |-> list_explicit_app
1365 | (head, args) => list_explicit_app head (map aux args)
1368 fun chop_fun 0 T = ([], T)
1369 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1370 chop_fun (n - 1) ran_T |>> cons dom_T
1371 | chop_fun _ _ = raise Fail "unexpected non-function"
1373 fun filter_type_args _ _ _ [] = []
1374 | filter_type_args thy s arity T_args =
1375 let val U = robust_const_type thy s in
1376 case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
1379 let val U_args = (s, U) |> Sign.const_typargs thy in
1381 |> map (fn (U, T) =>
1382 if member (op =) res_U_vars (dest_TVar U) then T
1386 handle TYPE _ => T_args
1388 fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
1390 val thy = Proof_Context.theory_of ctxt
1391 fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
1392 | aux arity (IConst (name as (s, _), T, T_args)) =
1393 (case strip_prefix_and_unascii const_prefix s of
1395 (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
1396 then [] else T_args)
1399 val s'' = invert_const s''
1400 fun filtered_T_args false = T_args
1401 | filtered_T_args true = filter_type_args thy s'' arity T_args
1403 case type_arg_policy type_enc s'' of
1404 Explicit_Type_Args drop_args =>
1405 (name, filtered_T_args drop_args)
1406 | Mangled_Type_Args drop_args =>
1407 (mangled_const_name format type_enc (filtered_T_args drop_args)
1409 | No_Type_Args => (name, [])
1411 |> (fn (name, T_args) => IConst (name, T, T_args))
1412 | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
1416 fun repair_iterm ctxt format type_enc sym_tab =
1417 not (is_type_enc_higher_order type_enc)
1418 ? (introduce_explicit_apps_in_iterm sym_tab
1419 #> introduce_predicators_in_iterm sym_tab)
1420 #> enforce_type_arg_policy_in_iterm ctxt format type_enc
1421 fun repair_fact ctxt format type_enc sym_tab =
1422 update_iformula (formula_map (repair_iterm ctxt format type_enc sym_tab))
1424 (** Helper facts **)
1426 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
1427 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
1429 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1431 [(("COMBI", false), @{thms Meson.COMBI_def}),
1432 (("COMBK", false), @{thms Meson.COMBK_def}),
1433 (("COMBB", false), @{thms Meson.COMBB_def}),
1434 (("COMBC", false), @{thms Meson.COMBC_def}),
1435 (("COMBS", false), @{thms Meson.COMBS_def}),
1436 ((predicator_name, false), [not_ffalse, ftrue]),
1437 (("fFalse", false), [not_ffalse]),
1438 (("fFalse", true), @{thms True_or_False}),
1439 (("fTrue", false), [ftrue]),
1440 (("fTrue", true), @{thms True_or_False}),
1442 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1443 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1445 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1446 by (unfold fconj_def) fast+}),
1448 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1449 by (unfold fdisj_def) fast+}),
1450 (("fimplies", false),
1451 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1452 by (unfold fimplies_def) fast+}),
1454 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1455 However, this is done so for backward compatibility: Including the
1456 equality helpers by default in Metis breaks a few existing proofs. *)
1457 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1458 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1459 (* Partial characterization of "fAll" and "fEx". A complete characterization
1460 would require the axiom of choice for replay with Metis. *)
1461 (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
1462 (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
1463 (("If", true), @{thms if_True if_False True_or_False})]
1464 |> map (apsnd (map zero_var_indexes))
1466 fun type_class_aterm type_enc class arg =
1468 Simple_Types (_, Polymorphic, _) =>
1469 if exploit_tff1_dummy_type_vars then ATerm (class, [arg])
1470 else ATerm (class, [arg, ATerm (TYPE_name, [arg])])
1471 | _ => ATerm (class, [arg])
1473 fun fo_literal_from_type_literal type_enc (TyLitVar (class, name)) =
1474 (true, type_class_aterm type_enc class (ATerm (name, [])))
1475 | fo_literal_from_type_literal type_enc (TyLitFree (class, name)) =
1476 (true, type_class_aterm type_enc class (ATerm (name, [])))
1477 (* FIXME: Really "true" in both cases? If so, merge "TyLitVar" and
1480 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
1482 fun bound_tvars type_enc Ts =
1483 mk_ahorn (map (formula_from_fo_literal
1484 o fo_literal_from_type_literal type_enc)
1485 (type_literals_for_types type_enc add_sorts_on_tvar Ts))
1487 fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
1488 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1489 else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
1490 |> bound_tvars type_enc atomic_Ts
1491 |> close_formula_universally type_enc
1493 val type_tag = `(make_fixed_const NONE) type_tag_name
1495 fun type_tag_idempotence_fact type_enc =
1497 fun var s = ATerm (`I s, [])
1498 fun tag tm = ATerm (type_tag, [var "A", tm])
1499 val tagged_var = tag (var "X")
1501 Formula (type_tag_idempotence_helper_name, Axiom,
1502 eq_formula type_enc [] false (tag tagged_var) tagged_var,
1503 isabelle_info simpN, NONE)
1506 fun should_specialize_helper type_enc t =
1507 polymorphism_of_type_enc type_enc <> Polymorphic andalso
1508 level_of_type_enc type_enc <> No_Types andalso
1509 not (null (Term.hidden_polymorphism t))
1511 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1512 case strip_prefix_and_unascii const_prefix s of
1515 val thy = Proof_Context.theory_of ctxt
1516 val unmangled_s = mangled_s |> unmangled_const_name
1517 fun dub needs_fairly_sound j k =
1518 (unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1519 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1520 (if needs_fairly_sound then typed_helper_suffix
1521 else untyped_helper_suffix),
1523 fun dub_and_inst needs_fairly_sound (th, j) =
1524 let val t = prop_of th in
1525 if should_specialize_helper type_enc t then
1526 map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
1531 |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
1532 val make_facts = map_filter (make_fact ctxt format type_enc false)
1533 val fairly_sound = is_type_enc_fairly_sound type_enc
1536 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1537 if helper_s <> unmangled_s orelse
1538 (needs_fairly_sound andalso not fairly_sound) then
1541 ths ~~ (1 upto length ths)
1542 |> maps (dub_and_inst needs_fairly_sound)
1546 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1547 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1550 (***************************************************************)
1551 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1552 (***************************************************************)
1554 fun set_insert (x, s) = Symtab.update (x, ()) s
1556 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1558 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1559 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1561 fun classes_of_terms get_Ts =
1562 map (map snd o get_Ts)
1563 #> List.foldl add_classes Symtab.empty
1564 #> delete_type #> Symtab.keys
1566 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
1567 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
1569 fun fold_type_constrs f (Type (s, Ts)) x =
1570 fold (fold_type_constrs f) Ts (f (s, x))
1571 | fold_type_constrs _ _ x = x
1573 (* Type constructors used to instantiate overloaded constants are the only ones
1575 fun add_type_constrs_in_term thy =
1577 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1578 | add (t $ u) = add t #> add u
1579 | add (Const (x as (s, _))) =
1580 if String.isPrefix skolem_const_prefix s then I
1581 else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
1582 | add (Free (s, T)) =
1583 if String.isPrefix polymorphic_free_prefix s then
1584 T |> fold_type_constrs set_insert
1587 | add (Abs (_, _, u)) = add u
1591 fun type_constrs_of_terms thy ts =
1592 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1594 fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
1595 hyp_ts concl_t facts =
1597 val thy = Proof_Context.theory_of ctxt
1598 val presimp_consts = Meson.presimplified_consts ctxt
1599 val fact_ts = facts |> map snd
1600 (* Remove existing facts from the conjecture, as this can dramatically
1601 boost an ATP's performance (for some reason). *)
1604 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1605 val facts = facts |> map (apsnd (pair Axiom))
1607 map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
1608 |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
1609 val ((conjs, facts), lambdas) =
1612 |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
1613 |> preprocess_abstractions_in_terms trans_lambdas
1614 |>> chop (length conjs)
1615 |>> apfst (map (apsnd (apsnd freeze_term)))
1617 ((conjs, facts), [])
1618 val conjs = conjs |> make_conjecture thy format type_enc
1619 val (fact_names, facts) =
1621 |> map_filter (fn (name, (_, t)) =>
1622 make_fact ctxt format type_enc true (name, t)
1623 |> Option.map (pair name))
1626 lambdas |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
1627 val all_ts = concl_t :: hyp_ts @ fact_ts
1628 val subs = tfree_classes_of_terms all_ts
1629 val supers = tvar_classes_of_terms all_ts
1630 val tycons = type_constrs_of_terms thy all_ts
1631 val (supers, arity_clauses) =
1632 if level_of_type_enc type_enc = No_Types then ([], [])
1633 else make_arity_clauses thy tycons supers
1634 val class_rel_clauses = make_class_rel_clauses thy subs supers
1636 (fact_names |> map single, union (op =) subs supers, conjs, facts @ lambdas,
1637 class_rel_clauses, arity_clauses)
1640 val type_guard = `(make_fixed_const NONE) type_guard_name
1642 fun type_guard_iterm ctxt format type_enc T tm =
1643 IApp (IConst (type_guard, T --> @{typ bool}, [T])
1644 |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
1646 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1647 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1648 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1649 | is_var_positively_naked_in_term _ _ _ _ = true
1651 fun should_guard_var_in_formula pos phi (SOME true) name =
1652 formula_fold pos (is_var_positively_naked_in_term name) phi false
1653 | should_guard_var_in_formula _ _ _ _ = true
1655 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
1656 | should_generate_tag_bound_decl ctxt mono (Tags (_, level, Nonuniform)) _ T =
1657 should_encode_type ctxt mono level T
1658 | should_generate_tag_bound_decl _ _ _ _ _ = false
1660 fun mk_aterm format type_enc name T_args args =
1661 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1663 fun tag_with_type ctxt format mono type_enc pos T tm =
1664 IConst (type_tag, T --> T, [T])
1665 |> enforce_type_arg_policy_in_iterm ctxt format type_enc
1666 |> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos)
1667 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1668 | _ => raise Fail "unexpected lambda-abstraction")
1669 and ho_term_from_iterm ctxt format mono type_enc =
1673 val (head, args) = strip_iterm_comb u
1676 Top_Level pos => pos
1681 IConst (name as (s, _), _, T_args) =>
1683 val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1685 mk_aterm format type_enc name T_args (map (aux arg_site) args)
1688 mk_aterm format type_enc name [] (map (aux Elsewhere) args)
1689 | IAbs ((name, T), tm) =>
1690 AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1692 | IApp _ => raise Fail "impossible \"IApp\""
1695 t |> (if should_tag_with_type ctxt mono type_enc site u T then
1696 tag_with_type ctxt format mono type_enc pos T
1701 and formula_from_iformula ctxt format mono type_enc should_guard_var =
1703 val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
1706 Simple_Types (_, _, level) => fused_type ctxt mono level 0
1707 #> ho_type_from_typ format type_enc false 0 #> SOME
1709 fun do_out_of_bound_type pos phi universal (name, T) =
1710 if should_guard_type ctxt mono type_enc
1711 (fn () => should_guard_var pos phi universal name) T then
1713 |> type_guard_iterm ctxt format type_enc T
1714 |> do_term pos |> AAtom |> SOME
1715 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
1717 val var = ATerm (name, [])
1718 val tagged_var = var |> tag_with_type ctxt format mono type_enc pos T
1719 in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
1722 fun do_formula pos (AQuant (q, xs, phi)) =
1724 val phi = phi |> do_formula pos
1725 val universal = Option.map (q = AExists ? not) pos
1727 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1728 | SOME T => do_bound_type T)),
1729 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1731 (fn (_, NONE) => NONE
1733 do_out_of_bound_type pos phi universal (s, T))
1737 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1738 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1741 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1742 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1743 the remote provers might care. *)
1744 fun formula_line_for_fact ctxt format prefix encode freshen pos mono type_enc
1745 (j, {name, locality, kind, iformula, atomic_types}) =
1746 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
1748 |> close_iformula_universally
1749 |> formula_from_iformula ctxt format mono type_enc
1750 should_guard_var_in_formula
1751 (if pos then SOME true else NONE)
1752 |> bound_tvars type_enc atomic_types
1753 |> close_formula_universally type_enc,
1756 Intro => isabelle_info introN
1757 | Elim => isabelle_info elimN
1758 | Simp => isabelle_info simpN
1762 fun formula_line_for_class_rel_clause type_enc
1763 ({name, subclass, superclass, ...} : class_rel_clause) =
1764 let val ty_arg = ATerm (tvar_a_name, []) in
1765 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1767 [AAtom (type_class_aterm type_enc subclass ty_arg),
1768 AAtom (type_class_aterm type_enc superclass ty_arg)])
1769 |> close_formula_universally type_enc, isabelle_info introN, NONE)
1772 fun fo_literal_from_arity_literal type_enc (AryLitConst (class, t, args)) =
1773 (true, type_class_aterm type_enc class
1774 (ATerm (t, map (fn arg => ATerm (arg, [])) args)))
1775 | fo_literal_from_arity_literal type_enc (AryLitVar (class, var)) =
1776 (false, type_class_aterm type_enc class (ATerm (var, [])))
1778 fun formula_line_for_arity_clause type_enc
1779 ({name, prem_lits, concl_lits, ...} : arity_clause) =
1780 Formula (arity_clause_prefix ^ name, Axiom,
1781 mk_ahorn (map (formula_from_fo_literal o apfst not
1782 o fo_literal_from_arity_literal type_enc) prem_lits)
1783 (formula_from_fo_literal
1784 (fo_literal_from_arity_literal type_enc concl_lits))
1785 |> close_formula_universally type_enc, isabelle_info introN, NONE)
1787 fun formula_line_for_conjecture ctxt format mono type_enc
1788 ({name, kind, iformula, atomic_types, ...} : translated_formula) =
1789 Formula (conjecture_prefix ^ name, kind,
1790 formula_from_iformula ctxt format mono type_enc
1791 should_guard_var_in_formula (SOME false)
1792 (close_iformula_universally iformula)
1793 |> bound_tvars type_enc atomic_types
1794 |> close_formula_universally type_enc, NONE, NONE)
1796 fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
1797 atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
1798 |> map (fo_literal_from_type_literal type_enc)
1800 fun formula_line_for_free_type j lit =
1801 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
1802 formula_from_fo_literal lit, NONE, NONE)
1803 fun formula_lines_for_free_types type_enc facts =
1805 val litss = map (free_type_literals type_enc) facts
1806 val lits = fold (union (op =)) litss []
1807 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
1809 (** Symbol declarations **)
1811 fun decl_line_for_class s =
1812 let val name as (s, _) = `make_type_class s in
1813 Decl (sym_decl_prefix ^ s, name,
1814 if exploit_tff1_dummy_type_vars then
1815 AFun (atype_of_types, bool_atype)
1817 ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)))
1820 fun decl_lines_for_classes type_enc classes =
1822 Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes
1825 fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
1828 fun add_iterm_syms in_conj tm =
1829 let val (head, args) = strip_iterm_comb tm in
1831 IConst ((s, s'), T, T_args) =>
1833 val pred_sym = is_pred_sym repaired_sym_tab s
1836 Guards _ => not pred_sym
1837 | _ => true) andalso
1838 is_tptp_user_symbol s
1841 Symtab.map_default (s, [])
1842 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
1847 | IAbs (_, tm) => add_iterm_syms in_conj tm
1849 #> fold (add_iterm_syms in_conj) args
1851 fun add_fact_syms in_conj =
1852 K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift
1853 fun add_formula_var_types (AQuant (_, xs, phi)) =
1854 fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
1855 #> add_formula_var_types phi
1856 | add_formula_var_types (AConn (_, phis)) =
1857 fold add_formula_var_types phis
1858 | add_formula_var_types _ = I
1860 if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
1861 else fold (fact_lift add_formula_var_types) (conjs @ facts) []
1862 fun add_undefined_const T =
1865 `(make_fixed_const NONE) @{const_name undefined}
1866 |> (case type_arg_policy type_enc @{const_name undefined} of
1867 Mangled_Type_Args _ => mangled_const_name format type_enc [T]
1870 Symtab.map_default (s, [])
1871 (insert_type ctxt #3 (s', [T], T, false, 0, false))
1873 fun add_TYPE_const () =
1874 let val (s, s') = TYPE_name in
1875 Symtab.map_default (s, [])
1876 (insert_type ctxt #3
1877 (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
1881 |> is_type_enc_fairly_sound type_enc
1882 ? (fold (add_fact_syms true) conjs
1883 #> fold (add_fact_syms false) facts
1884 #> (case type_enc of
1885 Simple_Types (_, poly, _) =>
1886 if poly = Polymorphic then add_TYPE_const () else I
1887 | _ => fold add_undefined_const (var_types ())))
1890 (* We add "bool" in case the helper "True_or_False" is included later. *)
1892 {maybe_finite_Ts = [@{typ bool}],
1893 surely_finite_Ts = [@{typ bool}],
1894 maybe_infinite_Ts = known_infinite_types,
1895 surely_infinite_Ts = known_infinite_types,
1896 maybe_nonmono_Ts = [@{typ bool}]}
1898 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
1899 out with monotonicity" paper presented at CADE 2011. *)
1900 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
1901 | add_iterm_mononotonicity_info ctxt level _
1902 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
1903 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
1904 surely_infinite_Ts, maybe_nonmono_Ts}) =
1905 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
1907 Noninf_Nonmono_Types soundness =>
1908 if exists (type_instance ctxt T) surely_infinite_Ts orelse
1909 member (type_aconv ctxt) maybe_finite_Ts T then
1911 else if is_type_kind_of_surely_infinite ctxt soundness
1912 surely_infinite_Ts T then
1913 {maybe_finite_Ts = maybe_finite_Ts,
1914 surely_finite_Ts = surely_finite_Ts,
1915 maybe_infinite_Ts = maybe_infinite_Ts,
1916 surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
1917 maybe_nonmono_Ts = maybe_nonmono_Ts}
1919 {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T,
1920 surely_finite_Ts = surely_finite_Ts,
1921 maybe_infinite_Ts = maybe_infinite_Ts,
1922 surely_infinite_Ts = surely_infinite_Ts,
1923 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
1924 | Fin_Nonmono_Types =>
1925 if exists (type_instance ctxt T) surely_finite_Ts orelse
1926 member (type_aconv ctxt) maybe_infinite_Ts T then
1928 else if is_type_surely_finite ctxt T then
1929 {maybe_finite_Ts = maybe_finite_Ts,
1930 surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
1931 maybe_infinite_Ts = maybe_infinite_Ts,
1932 surely_infinite_Ts = surely_infinite_Ts,
1933 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
1935 {maybe_finite_Ts = maybe_finite_Ts,
1936 surely_finite_Ts = surely_finite_Ts,
1937 maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_aconv ctxt) T,
1938 surely_infinite_Ts = surely_infinite_Ts,
1939 maybe_nonmono_Ts = maybe_nonmono_Ts}
1943 | add_iterm_mononotonicity_info _ _ _ _ mono = mono
1944 fun add_fact_mononotonicity_info ctxt level
1945 ({kind, iformula, ...} : translated_formula) =
1946 formula_fold (SOME (kind <> Conjecture))
1947 (add_iterm_mononotonicity_info ctxt level) iformula
1948 fun mononotonicity_info_for_facts ctxt type_enc facts =
1949 let val level = level_of_type_enc type_enc in
1951 |> is_type_level_monotonicity_based level
1952 ? fold (add_fact_mononotonicity_info ctxt level) facts
1955 fun add_iformula_monotonic_types ctxt mono type_enc =
1957 val level = level_of_type_enc type_enc
1958 val should_encode = should_encode_type ctxt mono level
1959 fun add_type T = not (should_encode T) ? insert_type ctxt I T
1960 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
1962 and add_term tm = add_type (ityp_of tm) #> add_args tm
1963 in formula_fold NONE (K add_term) end
1964 fun add_fact_monotonic_types ctxt mono type_enc =
1965 add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
1966 fun monotonic_types_for_facts ctxt mono type_enc facts =
1967 [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
1968 is_type_level_monotonicity_based (level_of_type_enc type_enc))
1969 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
1971 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
1972 Formula (guards_sym_formula_prefix ^
1973 ascii_of (mangled_type format type_enc T),
1975 IConst (`make_bound_var "X", T, [])
1976 |> type_guard_iterm ctxt format type_enc T
1978 |> formula_from_iformula ctxt format mono type_enc
1979 (K (K (K (K true)))) (SOME true)
1980 |> bound_tvars type_enc (atyps_of T)
1981 |> close_formula_universally type_enc,
1982 isabelle_info introN, NONE)
1984 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
1985 let val x_var = ATerm (`make_bound_var "X", []) in
1986 Formula (tags_sym_formula_prefix ^
1987 ascii_of (mangled_type format type_enc T),
1989 eq_formula type_enc (atyps_of T) false
1990 (tag_with_type ctxt format mono type_enc NONE T x_var)
1992 isabelle_info simpN, NONE)
1995 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
1997 Simple_Types _ => []
1999 map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
2000 | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
2002 fun decl_line_for_sym ctxt format mono type_enc s
2003 (s', T_args, T, pred_sym, ary, _) =
2005 val thy = Proof_Context.theory_of ctxt
2009 else case strip_prefix_and_unascii const_prefix s of
2012 val s' = s' |> invert_const
2013 val T = s' |> robust_const_type thy
2014 in (T, robust_const_typargs thy (s', T)) end
2016 case strip_prefix_and_unascii fixed_var_prefix s of
2018 if String.isPrefix polymorphic_free_prefix s' then (tvar_a, [tvar_a])
2019 else raise Fail "unexpected type arguments to free variable"
2020 | NONE => raise Fail "unexpected type arguments"
2022 Decl (sym_decl_prefix ^ s, (s, s'),
2023 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
2024 |> ho_type_from_typ format type_enc pred_sym ary
2025 |> not (null T_args)
2026 ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
2029 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
2030 j (s', T_args, T, _, ary, in_conj) =
2032 val (kind, maybe_negate) =
2033 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
2035 val (arg_Ts, res_T) = chop_fun ary T
2036 val num_args = length arg_Ts
2038 1 upto num_args |> map (`I o make_bound_var o string_of_int)
2040 bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
2041 val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
2042 fun should_keep_arg_type T =
2043 sym_needs_arg_types andalso
2044 should_guard_type ctxt mono type_enc (K true) T
2046 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
2048 Formula (guards_sym_formula_prefix ^ s ^
2049 (if n > 1 then "_" ^ string_of_int j else ""), kind,
2050 IConst ((s, s'), T, T_args)
2051 |> fold (curry (IApp o swap)) bounds
2052 |> type_guard_iterm ctxt format type_enc res_T
2053 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
2054 |> formula_from_iformula ctxt format mono type_enc
2055 (K (K (K (K true)))) (SOME true)
2056 |> n > 1 ? bound_tvars type_enc (atyps_of T)
2057 |> close_formula_universally type_enc
2059 isabelle_info introN, NONE)
2062 fun formula_lines_for_nonuniform_tags_sym_decl ctxt format conj_sym_kind mono
2063 type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
2066 tags_sym_formula_prefix ^ s ^
2067 (if n > 1 then "_" ^ string_of_int j else "")
2068 val (kind, maybe_negate) =
2069 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
2071 val (arg_Ts, res_T) = chop_fun ary T
2073 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
2074 val bounds = bound_names |> map (fn name => ATerm (name, []))
2075 val cst = mk_aterm format type_enc (s, s') T_args
2076 val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
2078 should_encode_type ctxt mono (level_of_type_enc type_enc)
2079 val tag_with = tag_with_type ctxt format mono type_enc NONE
2080 val add_formula_for_res =
2081 if should_encode res_T then
2082 cons (Formula (ident_base ^ "_res", kind,
2083 eq (tag_with res_T (cst bounds)) (cst bounds),
2084 isabelle_info simpN, NONE))
2087 fun add_formula_for_arg k =
2088 let val arg_T = nth arg_Ts k in
2089 if should_encode arg_T then
2090 case chop k bounds of
2091 (bounds1, bound :: bounds2) =>
2092 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
2093 eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
2095 isabelle_info simpN, NONE))
2096 | _ => raise Fail "expected nonempty tail"
2101 [] |> not pred_sym ? add_formula_for_res
2102 |> Config.get ctxt type_tag_arguments
2103 ? fold add_formula_for_arg (ary - 1 downto 0)
2106 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
2108 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
2112 decls |> map (decl_line_for_sym ctxt format mono type_enc s)
2113 | Guards (_, level, _) =>
2117 decl :: (decls' as _ :: _) =>
2118 let val T = result_type_of_decl decl in
2119 if forall (type_generalization ctxt T o result_type_of_decl)
2126 val n = length decls
2128 decls |> filter (should_encode_type ctxt mono level
2129 o result_type_of_decl)
2131 (0 upto length decls - 1, decls)
2132 |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
2135 | Tags (_, _, uniformity) =>
2139 let val n = length decls in
2140 (0 upto n - 1 ~~ decls)
2141 |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
2142 conj_sym_kind mono type_enc n s)
2145 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
2146 mono_Ts sym_decl_tab =
2148 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
2150 problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
2152 fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
2155 in mono_lines @ decl_lines end
2157 fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
2158 Config.get ctxt type_tag_idempotence andalso
2159 poly <> Mangled_Monomorphic andalso
2160 ((level = All_Types andalso uniformity = Nonuniform) orelse
2161 is_type_level_monotonicity_based level)
2162 | needs_type_tag_idempotence _ _ = false
2164 fun offset_of_heading_in_problem _ [] j = j
2165 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
2166 if heading = needle then j
2167 else offset_of_heading_in_problem needle problem (j + length lines)
2169 val implicit_declsN = "Should-be-implicit typings"
2170 val explicit_declsN = "Explicit typings"
2171 val factsN = "Relevant facts"
2172 val class_relsN = "Class relationships"
2173 val aritiesN = "Arities"
2174 val helpersN = "Helper facts"
2175 val conjsN = "Conjectures"
2176 val free_typesN = "Type variables"
2178 val explicit_apply = NONE (* for experiments *)
2180 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
2181 lambda_trans readable_names preproc hyp_ts concl_t facts =
2183 val type_enc = type_enc |> adjust_type_enc format
2185 if lambda_trans = smartN then
2186 if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
2187 else if lambda_trans = lambdasN andalso
2188 not (is_type_enc_higher_order type_enc) then
2189 error ("Lambda translation method incompatible with first-order \
2194 if lambda_trans = no_lambdasN then
2196 else if lambda_trans = concealedN then
2197 lift_lambdas ctxt type_enc ##> K []
2198 else if lambda_trans = liftingN then
2199 lift_lambdas ctxt type_enc
2200 else if lambda_trans = combinatorsN then
2201 map (introduce_combinators ctxt) #> rpair []
2202 else if lambda_trans = hybridN then
2203 lift_lambdas ctxt type_enc
2204 ##> maps (fn t => [t, introduce_combinators ctxt
2205 (intentionalize_def t)])
2206 else if lambda_trans = lambdasN then
2207 map (Envir.eta_contract) #> rpair []
2209 error ("Unknown lambda translation method: " ^
2210 quote lambda_trans ^ ".")
2211 val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
2212 translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
2213 hyp_ts concl_t facts
2214 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
2215 val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
2216 val repair = repair_fact ctxt format type_enc sym_tab
2217 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
2218 val repaired_sym_tab =
2219 conjs @ facts |> sym_table_for_facts ctxt (SOME false)
2221 repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
2224 helpers @ conjs @ facts
2225 |> monotonic_types_for_facts ctxt mono type_enc
2226 val class_decl_lines = decl_lines_for_classes type_enc classes
2227 val sym_decl_lines =
2228 (conjs, helpers @ facts)
2229 |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
2230 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
2233 0 upto length helpers - 1 ~~ helpers
2234 |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
2236 |> (if needs_type_tag_idempotence ctxt type_enc then
2237 cons (type_tag_idempotence_fact type_enc)
2240 (* Reordering these might confuse the proof reconstruction code or the SPASS
2243 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
2245 map (formula_line_for_fact ctxt format fact_prefix ascii_of
2246 (not exporter) (not exporter) mono type_enc)
2247 (0 upto length facts - 1 ~~ facts)),
2249 map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
2250 (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
2251 (helpersN, helper_lines),
2253 map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
2254 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
2258 CNF => ensure_cnf_problem
2259 | CNF_UEQ => filter_cnf_ueq_problem
2261 | TFF (_, TFF_Implicit) => I
2262 | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
2264 val (problem, pool) = problem |> nice_atp_problem readable_names
2265 val helpers_offset = offset_of_heading_in_problem helpersN problem 0
2267 map_filter (fn (j, {name, ...}) =>
2268 if String.isSuffix typed_helper_suffix name then SOME j
2270 ((helpers_offset + 1 upto helpers_offset + length helpers)
2272 fun add_sym_arity (s, {min_ary, ...} : sym_info) =
2274 case strip_prefix_and_unascii const_prefix s of
2275 SOME s => Symtab.insert (op =) (s, min_ary)
2281 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
2282 offset_of_heading_in_problem conjsN problem 0,
2283 offset_of_heading_in_problem factsN problem 0,
2284 fact_names |> Vector.fromList,
2286 Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
2290 val conj_weight = 0.0
2291 val hyp_weight = 0.1
2292 val fact_min_weight = 0.2
2293 val fact_max_weight = 1.0
2294 val type_info_default_weight = 0.8
2296 fun add_term_weights weight (ATerm (s, tms)) =
2297 is_tptp_user_symbol s ? Symtab.default (s, weight)
2298 #> fold (add_term_weights weight) tms
2299 | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
2300 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
2301 formula_fold NONE (K (add_term_weights weight)) phi
2302 | add_problem_line_weights _ _ = I
2304 fun add_conjectures_weights [] = I
2305 | add_conjectures_weights conjs =
2306 let val (hyps, conj) = split_last conjs in
2307 add_problem_line_weights conj_weight conj
2308 #> fold (add_problem_line_weights hyp_weight) hyps
2311 fun add_facts_weights facts =
2313 val num_facts = length facts
2315 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
2316 / Real.fromInt num_facts
2318 map weight_of (0 upto num_facts - 1) ~~ facts
2319 |> fold (uncurry add_problem_line_weights)
2322 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
2323 fun atp_problem_weights problem =
2324 let val get = these o AList.lookup (op =) problem in
2326 |> add_conjectures_weights (get free_typesN @ get conjsN)
2327 |> add_facts_weights (get factsN)
2328 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
2329 [explicit_declsN, class_relsN, aritiesN]
2331 |> sort (prod_ord Real.compare string_ord o pairself swap)