1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 07 13:50:17 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 07 13:50:17 2011 +0200
1.3 @@ -236,6 +236,12 @@
1.4 | string_for_kind Hypothesis = "hypothesis"
1.5 | string_for_kind Conjecture = "conjecture"
1.6
1.7 +fun string_for_app format func args =
1.8 + if is_format_thf format then
1.9 + "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
1.10 + else
1.11 + func ^ "(" ^ commas args ^ ")"
1.12 +
1.13 fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
1.14 | flatten_type (ty as AFun (ty1 as AType _, ty2)) =
1.15 (case flatten_type ty2 of
1.16 @@ -247,16 +253,17 @@
1.17 | flatten_type _ =
1.18 raise Fail "unexpected higher-order type in first-order format"
1.19
1.20 -fun str_for_type ty =
1.21 +fun str_for_type format ty =
1.22 let
1.23 fun str _ (AType (s, [])) = s
1.24 | str _ (AType (s, tys)) =
1.25 - tys |> map (str false)
1.26 - |> (if s = tptp_product_type then
1.27 - space_implode (" " ^ tptp_product_type ^ " ")
1.28 - #> length tys > 1 ? enclose "(" ")"
1.29 - else
1.30 - commas #> enclose "(" ")" #> prefix s)
1.31 + let val ss = tys |> map (str false) in
1.32 + if s = tptp_product_type then
1.33 + ss |> space_implode (" " ^ tptp_product_type ^ " ")
1.34 + |> length ss > 1 ? enclose "(" ")"
1.35 + else
1.36 + string_for_app format s ss
1.37 + end
1.38 | str rhs (AFun (ty1, ty2)) =
1.39 str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
1.40 |> not rhs ? enclose "(" ")"
1.41 @@ -266,8 +273,8 @@
1.42 ss) ^ "]: " ^ str false ty
1.43 in str true ty end
1.44
1.45 -fun string_for_type (THF _) ty = str_for_type ty
1.46 - | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
1.47 +fun string_for_type (format as THF _) ty = str_for_type format ty
1.48 + | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty)
1.49 | string_for_type _ _ = raise Fail "unexpected type in untyped format"
1.50
1.51 fun string_for_quantifier AForall = tptp_forall
1.52 @@ -293,35 +300,27 @@
1.53
1.54 fun string_for_term _ (ATerm (s, [])) = s
1.55 | string_for_term format (ATerm (s, ts)) =
1.56 - if s = tptp_empty_list then
1.57 - (* used for lists in the optional "source" field of a derivation *)
1.58 - "[" ^ commas (map (string_for_term format) ts) ^ "]"
1.59 - else if is_tptp_equal s then
1.60 - space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
1.61 - |> is_format_thf format ? enclose "(" ")"
1.62 - else
1.63 - (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
1.64 - s = tptp_choice andalso is_format_with_choice format, ts) of
1.65 - (true, _, [AAbs ((s', ty), tm)]) =>
1.66 - (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
1.67 - possible, to work around LEO-II 1.2.8 parser limitation. *)
1.68 - string_for_formula format
1.69 - (AQuant (if s = tptp_ho_forall then AForall else AExists,
1.70 - [(s', SOME ty)], AAtom tm))
1.71 - | (_, true, [AAbs ((s', ty), tm)]) =>
1.72 - (* There is code in "ATP_Translate" to ensure that "Eps" is always
1.73 - applied to an abstraction. *)
1.74 - tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
1.75 - string_for_term format tm ^ ""
1.76 - |> enclose "(" ")"
1.77 -
1.78 - | _ =>
1.79 - let val ss = map (string_for_term format) ts in
1.80 - if is_format_thf format then
1.81 - "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
1.82 - else
1.83 - s ^ "(" ^ commas ss ^ ")"
1.84 - end)
1.85 + (if s = tptp_empty_list then
1.86 + (* used for lists in the optional "source" field of a derivation *)
1.87 + "[" ^ commas (map (string_for_term format) ts) ^ "]"
1.88 + else if is_tptp_equal s then
1.89 + space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
1.90 + |> is_format_thf format ? enclose "(" ")"
1.91 + else case (s = tptp_ho_forall orelse s = tptp_ho_exists,
1.92 + s = tptp_choice andalso is_format_with_choice format, ts) of
1.93 + (true, _, [AAbs ((s', ty), tm)]) =>
1.94 + (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
1.95 + possible, to work around LEO-II 1.2.8 parser limitation. *)
1.96 + string_for_formula format
1.97 + (AQuant (if s = tptp_ho_forall then AForall else AExists,
1.98 + [(s', SOME ty)], AAtom tm))
1.99 + | (_, true, [AAbs ((s', ty), tm)]) =>
1.100 + (* There is code in "ATP_Translate" to ensure that "Eps" is always
1.101 + applied to an abstraction. *)
1.102 + tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
1.103 + string_for_term format tm ^ ""
1.104 + |> enclose "(" ")"
1.105 + | _ => string_for_app format s (map (string_for_term format) ts))
1.106 | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
1.107 "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
1.108 string_for_term format tm ^ ")"