--- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 00:01:33 2011 +0200
@@ -15,11 +15,13 @@
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 format = CNF_UEQ | FOF | TFF | THF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
- Decl of string * 'a * 'a list * 'a |
- Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
+ Decl of string * 'a * 'a ho_type |
+ Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list
@@ -30,6 +32,7 @@
val tptp_type_of_types : string
val tptp_bool_type : string
val tptp_individual_type : string
+ val tptp_fun_type : string
val is_atp_variable : string -> bool
val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
val mk_aconn :
@@ -61,11 +64,13 @@
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 format = CNF_UEQ | FOF | TFF | THF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
- Decl of string * 'a * 'a list * 'a |
- Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
+ Decl of string * 'a * 'a ho_type |
+ Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list
@@ -76,6 +81,7 @@
val tptp_type_of_types = "$tType"
val tptp_bool_type = "$o"
val tptp_individual_type = "$i"
+val tptp_fun_type = ">"
fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
@@ -102,6 +108,25 @@
| 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 _, _)) =
+ raise Fail "unexpected higher-order type in first-order format"
+ | strip_tff_type (AType s) = ([], s)
+
+fun string_for_type THF 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
+ | string_for_type TFF ty =
+ (case strip_tff_type ty of
+ ([], s) => s
+ | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
+ | (ss, s) => "(" ^ space_implode " * " ss ^ ") " ^ tptp_fun_type ^ " " ^ s)
+ | string_for_type _ _ = raise Fail "unexpected type in untyped format"
+
fun string_for_term _ (ATerm (s, [])) = s
| string_for_term format (ATerm ("equal", ts)) =
space_implode " = " (map (string_for_term format) ts)
@@ -114,8 +139,10 @@
if format = THF then "(" ^ space_implode " @ " (s :: ss) ^ ")"
else s ^ "(" ^ commas ss ^ ")"
end
+
fun string_for_quantifier AForall = "!"
| string_for_quantifier AExists = "?"
+
fun string_for_connective ANot = "~"
| string_for_connective AAnd = "&"
| string_for_connective AOr = "|"
@@ -123,17 +150,21 @@
| string_for_connective AIf = "<="
| string_for_connective AIff = "<=>"
| string_for_connective ANotIff = "<~>"
+
fun string_for_bound_var format (s, ty) =
- s ^ (if format = TFF orelse format = THF then
- " : " ^ (ty |> the_default tptp_individual_type)
- else
- "")
+ s ^ (if format = TFF orelse format = THF then
+ " : " ^
+ string_for_type format (ty |> the_default (AType tptp_individual_type))
+ else
+ "")
+
fun string_for_formula format (AQuant (q, xs, phi)) =
"(" ^ string_for_quantifier q ^
"[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
string_for_formula format phi ^ ")"
| string_for_formula format (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
space_implode " != " (map (string_for_term format) ts)
+ |> format = THF ? enclose "(" ")"
| string_for_formula format (AConn (c, [phi])) =
"(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")"
| string_for_formula format (AConn (c, phis)) =
@@ -141,14 +172,6 @@
(map (string_for_formula format) phis) ^ ")"
| string_for_formula format (AAtom tm) = string_for_term format tm
-fun string_for_symbol_type THF arg_tys res_ty =
- space_implode " > " (arg_tys @ [res_ty])
- | string_for_symbol_type _ [] res_ty = res_ty
- | string_for_symbol_type _ [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
- | string_for_symbol_type format arg_tys res_ty =
- string_for_symbol_type format ["(" ^ space_implode " * " arg_tys ^ ")"]
- res_ty
-
val default_source =
ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
@@ -157,9 +180,9 @@
| string_for_format TFF = "tff"
| string_for_format THF = "thf"
-fun string_for_problem_line format (Decl (ident, sym, arg_tys, res_ty)) =
+fun string_for_problem_line format (Decl (ident, sym, ty)) =
string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
- string_for_symbol_type format arg_tys res_ty ^ ").\n"
+ string_for_type format ty ^ ").\n"
| string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^
",\n (" ^ string_for_formula format phi ^ ")" ^
@@ -285,20 +308,20 @@
fun nice_term (ATerm (name, ts)) =
nice_name name ##>> pool_map nice_term ts #>> ATerm
+fun nice_type (AType name) = nice_name name #>> AType
+ | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
fun nice_formula (AQuant (q, xs, phi)) =
pool_map nice_name (map fst xs)
##>> pool_map (fn NONE => pair NONE
- | SOME ty => nice_name ty #>> SOME) (map snd xs)
+ | SOME ty => nice_type ty #>> SOME) (map snd xs)
##>> nice_formula phi
#>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
| nice_formula (AConn (c, phis)) =
pool_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom
-fun nice_problem_line (Decl (ident, sym, arg_tys, res_ty)) =
- nice_name sym
- ##>> pool_map nice_name arg_tys
- ##>> nice_name res_ty
- #>> (fn ((sym, arg_tys), res_ty) => Decl (ident, sym, arg_tys, res_ty))
+fun nice_problem_line (Decl (ident, sym, ty)) =
+ nice_name sym ##>> nice_type ty
+ #>> (fn (sym, ty) => Decl (ident, sym, ty))
| nice_problem_line (Formula (ident, kind, phi, source, info)) =
nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
fun nice_problem problem =
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue May 24 00:01:33 2011 +0200
@@ -462,7 +462,8 @@
val atps =
[e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
- remote_leo2, remote_sine_e, remote_snark, remote_tofof_e, remote_waldmeister]
+ remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e,
+ remote_waldmeister]
val setup = fold add_atp atps
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 24 00:01:33 2011 +0200
@@ -99,7 +99,8 @@
val simple_type_prefix = "ty_"
fun make_simple_type s =
- if s = tptp_bool_type then s else simple_type_prefix ^ ascii_of s
+ if s = tptp_bool_type orelse s = tptp_fun_type then s
+ else simple_type_prefix ^ ascii_of s
(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"
@@ -281,8 +282,10 @@
fun close_formula_universally phi = close_universally term_vars phi
fun fo_term_from_typ format (Type (s, Ts)) =
- ATerm (if format = THF andalso s = @{type_name bool} then `I tptp_bool_type
- else `make_fixed_type_const s,
+ ATerm (case (format, s) of
+ (THF, @{type_name bool}) => `I tptp_bool_type
+ | (THF, @{type_name fun}) => `I tptp_fun_type
+ | _ => `make_fixed_type_const s,
map (fo_term_from_typ format) Ts)
| fo_term_from_typ _ (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
| fo_term_from_typ _ (TVar ((x as (s, _)), _)) =
@@ -295,19 +298,30 @@
| generic_mangled_type_name f (ATerm (name, tys)) =
f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
^ ")"
-fun mangled_type_name format =
- fo_term_from_typ format
- #> (fn ty => (make_simple_type (generic_mangled_type_name fst ty),
- generic_mangled_type_name snd ty))
-fun generic_mangled_type_suffix f g Ts =
- fold_rev (curry (op ^) o g o prefix mangled_type_sep
- o generic_mangled_type_name f) Ts ""
+fun ho_type_from_fo_term format pred_sym ary =
+ let
+ fun to_atype ty =
+ AType ((make_simple_type (generic_mangled_type_name fst ty),
+ generic_mangled_type_name snd ty))
+ fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
+ fun to_tff 0 ty =
+ if pred_sym then AType (`I tptp_bool_type) else to_atype ty
+ | to_tff ary (ATerm (_, tys)) = to_afun to_atype (to_tff (ary - 1)) tys
+ fun to_thf (ty as ATerm ((s, _), tys)) =
+ if s = tptp_fun_type then to_afun to_thf to_thf tys else to_atype ty
+ in if format = THF then to_thf else to_tff ary end
+
+fun mangled_type format pred_sym ary =
+ ho_type_from_fo_term format pred_sym ary o fo_term_from_typ format
+
fun mangled_const_name format T_args (s, s') =
- let val ty_args = map (fo_term_from_typ format) T_args in
- (s ^ generic_mangled_type_suffix fst ascii_of ty_args,
- s' ^ generic_mangled_type_suffix snd I ty_args)
- end
+ let
+ val ty_args = map (fo_term_from_typ format) T_args
+ fun type_suffix f g =
+ fold_rev (curry (op ^) o g o prefix mangled_type_sep
+ o generic_mangled_type_name f) ty_args ""
+ in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
val parse_mangled_ident =
Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
@@ -334,12 +348,15 @@
fun introduce_proxies format tm =
let
- fun aux top_level (CombApp (tm1, tm2)) =
- CombApp (aux top_level tm1, aux false tm2)
- | aux top_level (CombConst (name as (s, s'), T, T_args)) =
+ fun aux ary top_level (CombApp (tm1, tm2)) =
+ CombApp (aux (ary + 1) top_level tm1, aux 0 false tm2)
+ | aux ary top_level (CombConst (name as (s, s'), T, T_args)) =
(case proxify_const s of
SOME proxy_base =>
- if top_level orelse format = THF then
+ (* Proxies are not needed in THF, except for partially applied
+ equality since THF does not provide any syntax for it. *)
+ if top_level orelse
+ (format = THF andalso (s <> "equal" orelse ary = 2)) then
(case s of
"c_False" => (tptp_false, s')
| "c_True" => (tptp_true, s')
@@ -348,8 +365,8 @@
(proxy_base |>> prefix const_prefix, T_args)
| NONE => (name, T_args))
|> (fn (name, T_args) => CombConst (name, T, T_args))
- | aux _ tm = tm
- in aux true tm end
+ | aux _ _ tm = tm
+ in aux 0 true tm end
fun combformula_from_prop thy format eq_as_iff =
let
@@ -863,7 +880,8 @@
val do_bound_type =
case type_sys of
Simple_Types level =>
- SOME o mangled_type_name format o homogenized_type ctxt nonmono_Ts level
+ homogenized_type ctxt nonmono_Ts level
+ #> mangled_type format false 0 #> SOME
| _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
if should_predicate_on_type ctxt nonmono_Ts type_sys
@@ -1041,15 +1059,9 @@
fun decl_line_for_sym ctxt format nonmono_Ts level s
(s', _, T, pred_sym, ary, _) =
- let
- val translate_type =
- mangled_type_name format o homogenized_type ctxt nonmono_Ts level
- val (arg_tys, res_ty) =
- T |> chop_fun ary |>> map translate_type ||> translate_type
- in
- Decl (sym_decl_prefix ^ s, (s, s'), arg_tys,
- if pred_sym then `I tptp_bool_type else res_ty)
- end
+ Decl (sym_decl_prefix ^ s, (s, s'),
+ T |> homogenized_type ctxt nonmono_Ts level
+ |> mangled_type format pred_sym ary)
fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
@@ -1073,8 +1085,7 @@
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bounds
|> type_pred_combterm ctxt format nonmono_Ts type_sys res_T
- |> AAtom
- |> mk_aquant AForall (bound_names ~~ bound_Ts)
+ |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
|> formula_from_combformula ctxt format nonmono_Ts type_sys
(K (K (K (K true)))) true
|> n > 1 ? bound_atomic_types format type_sys (atyps_of T)
@@ -1179,14 +1190,19 @@
type_sys)
sym_decl_tab []
+fun add_simple_types_in_type (AFun (ty1, ty2)) =
+ fold add_simple_types_in_type [ty1, ty2]
+ | add_simple_types_in_type (AType name) = insert (op =) name
+
fun add_simple_types_in_formula (AQuant (_, xs, phi)) =
- union (op =) (map_filter snd xs) #> add_simple_types_in_formula phi
+ fold add_simple_types_in_type (map_filter snd xs)
+ #> add_simple_types_in_formula phi
| add_simple_types_in_formula (AConn (_, phis)) =
fold add_simple_types_in_formula phis
| add_simple_types_in_formula (AAtom _) = I
-fun add_simple_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
- union (op =) (res_T :: arg_Ts)
+fun add_simple_types_in_problem_line (Decl (_, _, ty)) =
+ add_simple_types_in_type ty
| add_simple_types_in_problem_line (Formula (_, _, phi, _, _)) =
add_simple_types_in_formula phi
@@ -1195,7 +1211,7 @@
|> filter_out (String.isPrefix tptp_special_prefix o fst)
fun decl_line_for_simple_type (s, s') =
- Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_type_of_types)
+ Decl (type_decl_prefix ^ s, (s, s'), AType (`I tptp_type_of_types))
fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
level = Nonmonotonic_Types orelse level = Finite_Types
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 00:01:33 2011 +0200
@@ -439,23 +439,24 @@
[Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]
fun adjust_dumb_type_sys formats (Simple_Types level) =
- (case inter (op =) formats [TFF, THF] of
- format :: _ => (format, Simple_Types level)
- | [] => adjust_dumb_type_sys formats
- (Preds (Mangled_Monomorphic, level, Heavy)))
+ if member (op =) formats THF then
+ (THF, Simple_Types level)
+ else if member (op =) formats TFF then
+ (TFF, Simple_Types level)
+ else
+ adjust_dumb_type_sys formats (Preds (Mangled_Monomorphic, level, Heavy))
| adjust_dumb_type_sys formats type_sys =
- if member (op =) formats CNF_UEQ then
+ if member (op =) formats FOF then
+ (FOF, type_sys)
+ else if member (op =) formats CNF_UEQ then
(CNF_UEQ, case type_sys of
Tags _ => type_sys
| _ => Preds (polymorphism_of_type_sys type_sys,
Const_Arg_Types, Light))
- else if member (op =) formats FOF then
- (FOF, type_sys)
else
- (* We could return "type_sys" in all cases but this would require the
- TFF and THF provers to accept problems in which constants are
- implicitly declared. Today neither SNARK nor ToFoF-E satisfy this
- criterion. (FIXME: what about LEO-II?) *)
+ (* We could return "type_sys" unchanged for TFF but this would require the
+ TFF provers to accept problems in which constants are implicitly
+ declared. Today neither SNARK nor ToFoF-E meet this criterion. *)
(hd formats, Simple_Types All_Types)
fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
adjust_dumb_type_sys formats type_sys