--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 26 13:47:29 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 26 18:06:36 2020 +0100
@@ -97,6 +97,8 @@
val tptp_true : string
val tptp_lambda : string
val tptp_empty_list : string
+ val tptp_unary_builtins : string list
+ val tptp_binary_builtins : string list
val dfg_individual_type : string
val isabelle_info_prefix : string
val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
@@ -257,6 +259,10 @@
val tptp_lambda = "^"
val tptp_empty_list = "[]"
+val tptp_unary_builtins = [tptp_not]
+val tptp_binary_builtins =
+ [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal]
+
val dfg_individual_type = "iii" (* cannot clash *)
val isabelle_info_prefix = "isabelle_"
@@ -455,14 +461,8 @@
else
"")
-local
- val unary_builtins = [tptp_not]
- val binary_builtins =
- [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal]
- val builtins = unary_builtins @ binary_builtins
-in
-
-fun tptp_string_of_term _ (ATerm ((s, []), [])) = s |> member (op =) builtins s ? parens
+fun tptp_string_of_term _ (ATerm ((s, []), [])) =
+ s |> member (op =) (tptp_unary_builtins @ tptp_binary_builtins) s ? parens
| tptp_string_of_term format (ATerm ((s, tys), ts)) =
let
val of_type = string_of_type format
@@ -496,10 +496,10 @@
"]: " ^ of_term tm ^ ""
|> parens) (map of_term args)
| _ => app ())
- else if member (op =) unary_builtins s then
+ else if member (op =) tptp_unary_builtins s then
(* generate e.g. "~ t" instead of "~ @ t". *)
(case ts of [t] => s ^ " " ^ (of_term t |> parens) |> parens)
- else if member (op =) binary_builtins s then
+ else if member (op =) tptp_binary_builtins s then
(* generate e.g. "t1 & t2" instead of "& @ t1 @ t2". *)
(case ts of
[t1, t2] => (of_term t1 |> parens) ^ " " ^ s ^ " " ^ (of_term t2 |> parens) |> parens
@@ -541,8 +541,6 @@
|> parens
| tptp_string_of_formula format (AAtom tm) = tptp_string_of_term format tm
-end
-
fun tptp_string_of_format CNF = tptp_cnf
| tptp_string_of_format CNF_UEQ = tptp_cnf
| tptp_string_of_format FOF = tptp_fof
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 26 13:47:29 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 26 18:06:36 2020 +0100
@@ -1423,20 +1423,20 @@
(** predicators and application operators **)
-type sym_info =
- {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
- in_conj : bool}
+type sym_info = {pred_sym : bool, min_ary : int, max_ary : int, types : typ list, in_conj : bool}
fun default_sym_tab_entries type_enc =
- (make_fixed_const NONE \<^const_name>\<open>undefined\<close>,
- {pred_sym = false, min_ary = 0, max_ary = 0, types = [], in_conj = false}) ::
- ([tptp_false, tptp_true]
- |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @
- ([tptp_equal, tptp_old_equal]
- |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false}))
- |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
- ? cons (prefixed_predicator_name,
- {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false})
+ let
+ fun mk_sym_info pred n =
+ {pred_sym = pred, min_ary = n, max_ary = n, types = [], in_conj = false}
+ in
+ (make_fixed_const NONE \<^const_name>\<open>undefined\<close>, mk_sym_info false 0) ::
+ (map (rpair (mk_sym_info true 0)) [tptp_false, tptp_true]) @
+ (map (rpair (mk_sym_info true 1)) tptp_unary_builtins) @
+ (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins))
+ |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
+ ? cons (prefixed_predicator_name, mk_sym_info true 1)
+ end
datatype app_op_level =
Min_App_Op |