Tuned parentheses in TPTP output
authordesharna
Wed, 18 Nov 2020 13:44:34 +0100
changeset 72877 4eea17b3ac58
parent 72876 fffad9ad660e
child 72878 0e422e806ef3
child 72879 d152890dd17e
Tuned parentheses in TPTP output
src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Nov 17 23:26:41 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Nov 18 13:44:34 2020 +0100
@@ -370,6 +370,10 @@
   | is_format_typed (DFG _) = true
   | is_format_typed _ = false
 
+fun is_format_with_fool (THF (With_FOOL, _, _)) = true
+  | is_format_with_fool (TFF (With_FOOL, _)) = true
+  | is_format_with_fool _ = false
+
 fun tptp_string_of_role Axiom = "axiom"
   | tptp_string_of_role Definition = "definition"
   | tptp_string_of_role Lemma = "lemma"
@@ -465,7 +469,7 @@
         "[" ^ commas (map of_term ts) ^ "]"
       else if is_tptp_equal s then
         space_implode (" " ^ tptp_equal ^ " ") (map of_term ts)
-        |> is_format_higher_order format ? parens
+        |> (is_format_higher_order format orelse is_format_with_fool format) ? parens
       else if s = tptp_ho_forall orelse s = tptp_ho_exists then
         (case ts of
           [AAbs (((s', ty), tm), [])] =>