--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:45 2011 +0200
@@ -17,7 +17,9 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
- datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
+ datatype 'a ho_type =
+ AType of 'a * 'a ho_type list |
+ AFun of 'a ho_type * 'a ho_type
datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
datatype tff_explicitness = TFF_Implicit | TFF_Explicit
@@ -118,7 +120,9 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
-datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
+datatype 'a ho_type =
+ AType of 'a * 'a ho_type list |
+ AFun of 'a ho_type * 'a ho_type
datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
datatype tff_explicitness = TFF_Implicit | TFF_Explicit
@@ -225,25 +229,29 @@
| string_for_kind Hypothesis = "hypothesis"
| string_for_kind Conjecture = "conjecture"
-fun strip_tff_type (AFun (AType s, ty)) = strip_tff_type ty |>> cons s
- | strip_tff_type (AFun (AFun _, _)) =
+fun strip_tff_type (AFun (AFun _, _)) =
raise Fail "unexpected higher-order type in first-order format"
- | strip_tff_type (AType s) = ([], s)
+ | strip_tff_type (AFun (ty1, ty2)) = strip_tff_type ty2 |>> cons ty1
+ | strip_tff_type ty = ([], ty)
-fun string_for_type (THF0 _) ty =
- let
- fun aux _ (AType s) = s
- | aux rhs (AFun (ty1, ty2)) =
- aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2
- |> not rhs ? enclose "(" ")"
- in aux true ty end
+fun general_string_for_type ty =
+ let
+ fun str _ (AType (s, [])) = s
+ | str _ (AType (s, tys)) = s ^ "(" ^ commas (map (str false) tys) ^ ")"
+ | str rhs (AFun (ty1, ty2)) =
+ str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
+ |> not rhs ? enclose "(" ")"
+ in str true ty end
+
+fun string_for_type (THF0 _) ty = general_string_for_type ty
| string_for_type (TFF _) ty =
(case strip_tff_type ty of
- ([], s) => s
- | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
- | (ss, s) =>
- "(" ^ space_implode (" " ^ tptp_product_type ^ " ") ss ^ ") " ^
- tptp_fun_type ^ " " ^ s)
+ ([], ty) => general_string_for_type ty
+ | ([ty1], ty2) => general_string_for_type (AFun (ty1, ty2))
+ | (tys, ty) =>
+ "(" ^ space_implode (" " ^ tptp_product_type ^ " ")
+ (map general_string_for_type tys) ^ ") " ^ tptp_fun_type ^ " " ^
+ general_string_for_type ty)
| string_for_type _ _ = raise Fail "unexpected type in untyped format"
fun string_for_quantifier AForall = tptp_forall
@@ -256,11 +264,13 @@
| string_for_connective AIff = tptp_iff
fun string_for_bound_var format (s, ty) =
- s ^ (if is_format_typed format then
- " " ^ tptp_has_type ^ " " ^
- string_for_type format (ty |> the_default (AType tptp_individual_type))
- else
- "")
+ s ^
+ (if is_format_typed format then
+ " " ^ tptp_has_type ^ " " ^
+ (ty |> the_default (AType (tptp_individual_type, []))
+ |> string_for_type format)
+ else
+ "")
fun string_for_term _ (ATerm (s, [])) = s
| string_for_term format (ATerm (s, ts)) =
@@ -440,9 +450,9 @@
symbols (with "$i" as the type of individuals), but some provers (e.g.,
SNARK) require explicit declarations. The situation is similar for THF. *)
-val atype_of_types = AType (`I tptp_type_of_types)
-val bool_atype = AType (`I tptp_bool_type)
-val individual_atype = AType (`I tptp_individual_type)
+val atype_of_types = AType (`I tptp_type_of_types, [])
+val bool_atype = AType (`I tptp_bool_type, [])
+val individual_atype = AType (`I tptp_individual_type, [])
fun default_type pred_sym =
let
@@ -459,8 +469,9 @@
let
fun do_sym name ty =
if member (op =) declared name then I else AList.default (op =) (name, ty)
- fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2]
- | do_type (AType name) = do_sym name (K atype_of_types)
+ fun do_type (AType (name, tys)) =
+ do_sym name (K atype_of_types) #> fold do_type tys
+ | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
fun do_term pred_sym (ATerm (name as (s, _), tms)) =
is_tptp_user_symbol s
? do_sym name (fn _ => default_type pred_sym (length tms))
@@ -557,7 +568,8 @@
end
in add 0 |> apsnd SOME end
-fun nice_type (AType name) = nice_name name #>> AType
+fun nice_type (AType (name, tys)) =
+ nice_name name ##>> pool_map nice_type tys #>> AType
| nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
fun nice_term (ATerm (name, ts)) =
nice_name name ##>> pool_map nice_term ts #>> ATerm