# HG changeset patch # User blanchet # Date 1306188093 -7200 # Node ID 5725deb11ae73f7749f7687d839142705bcb3f98 # Parent 3b50fdeb6cfc8e07f4acde19d8028de5d35ed5f2 identify HOL functions with THF functions diff -r 3b50fdeb6cfc -r 5725deb11ae7 src/HOL/Tools/ATP/atp_problem.ML --- 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 = diff -r 3b50fdeb6cfc -r 5725deb11ae7 src/HOL/Tools/ATP/atp_systems.ML --- 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; diff -r 3b50fdeb6cfc -r 5725deb11ae7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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 diff -r 3b50fdeb6cfc -r 5725deb11ae7 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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