# HG changeset patch # User blanchet # Date 1306485007 -7200 # Node ID bd424c3dde464a88929e90faa46e401616341e2e # Parent 0db96016bdbfd3bba047e6b416e2e8e16aa802f0 cleaner handling of equality and proxies (esp. for THF) diff -r 0db96016bdbf -r bd424c3dde46 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri May 27 10:30:07 2011 +0200 @@ -47,8 +47,11 @@ val tptp_app : string val tptp_not_infix : string val tptp_equal : string + val tptp_old_equal : string val tptp_false : string val tptp_true : string + val tptp_empty_list : string + val is_tptp_equal : string -> bool val is_built_in_tptp_symbol : string -> bool val is_tptp_variable : string -> bool val is_tptp_user_symbol : string -> bool @@ -127,11 +130,14 @@ val tptp_app = "@" val tptp_not_infix = "!" val tptp_equal = "=" +val tptp_old_equal = "equal" val tptp_false = "$false" val tptp_true = "$true" +val tptp_empty_list = "[]" -fun is_built_in_tptp_symbol "equal" = true (* deprecated *) - | is_built_in_tptp_symbol s = not (Char.isAlpha (String.sub (s, 0))) +fun is_tptp_equal s = (s = tptp_equal orelse s = tptp_old_equal) +fun is_built_in_tptp_symbol s = + s = tptp_old_equal orelse not (Char.isAlpha (String.sub (s, 0))) fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol) @@ -203,19 +209,20 @@ | 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 (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts) - |> format = THF ? enclose "(" ")" - | string_for_term format (ATerm ("[]", ts)) = - (* used for lists in the optional "source" field of a derivation *) - "[" ^ commas (map (string_for_term format) ts) ^ "]" | string_for_term format (ATerm (s, ts)) = - let val ss = map (string_for_term format) ts in - if format = THF then - "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")" - else - s ^ "(" ^ commas ss ^ ")" - end + if s = tptp_empty_list then + (* used for lists in the optional "source" field of a derivation *) + "[" ^ commas (map (string_for_term format) ts) ^ "]" + else if is_tptp_equal s then + space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts) + |> format = THF ? enclose "(" ")" + else + let val ss = map (string_for_term format) ts in + if format = THF then + "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")" + else + s ^ "(" ^ commas ss ^ ")" + end fun string_for_quantifier AForall = tptp_forall | string_for_quantifier AExists = tptp_exists @@ -240,7 +247,8 @@ "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^ string_for_formula format phi |> enclose "(" ")" - | string_for_formula format (AConn (ANot, [AAtom (ATerm ("equal", ts))])) = + | string_for_formula format + (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) = space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") (map (string_for_term format) ts) |> format = THF ? enclose "(" ")" @@ -290,7 +298,7 @@ | is_problem_line_negated _ = false fun is_problem_line_cnf_ueq - (Formula (_, _, AAtom (ATerm (("equal", _), _)), _, _)) = true + (Formula (_, _, AAtom (ATerm ((s, _), _)), _, _)) = is_tptp_equal s | is_problem_line_cnf_ueq _ = false fun open_conjecture_term (ATerm ((s, s'), tms)) = @@ -392,10 +400,11 @@ (* Long names can slow down the ATPs. *) val max_readable_name_size = 20 -(* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the - problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure - that "HOL.eq" is correctly mapped to equality. *) -val reserved_nice_names = ["op", "equal", "eq"] +(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the + unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to + ensure that "HOL.eq" is correctly mapped to equality (not clear whether this + is still necessary). *) +val reserved_nice_names = [tptp_old_equal, "op", "eq"] fun readable_name full_name s = if s = full_name then diff -r 0db96016bdbf -r bd424c3dde46 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Fri May 27 10:30:07 2011 +0200 @@ -47,7 +47,7 @@ val type_const_prefix: string val class_prefix: string val new_skolem_const_prefix : string - val proxify_const : string -> (string * string) option + val proxify_const : string -> (int * (string * string)) option val invert_const: string -> string val unproxify_const: string -> string val ascii_of: string -> string @@ -109,14 +109,16 @@ fun union_all xss = fold (union (op =)) xss [] val metis_proxies = - [("c_False", (@{const_name False}, ("fFalse", @{const_name Metis.fFalse}))), - ("c_True", (@{const_name True}, ("fTrue", @{const_name Metis.fTrue}))), - ("c_Not", (@{const_name Not}, ("fNot", @{const_name Metis.fNot}))), - ("c_conj", (@{const_name conj}, ("fconj", @{const_name Metis.fconj}))), - ("c_disj", (@{const_name disj}, ("fdisj", @{const_name Metis.fdisj}))), - ("c_implies", (@{const_name implies}, - ("fimplies", @{const_name Metis.fimplies}))), - ("equal", (@{const_name HOL.eq}, ("fequal", @{const_name Metis.fequal})))] + [("c_False", + (@{const_name False}, (0, ("fFalse", @{const_name Metis.fFalse})))), + ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name Metis.fTrue})))), + ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name Metis.fNot})))), + ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name Metis.fconj})))), + ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name Metis.fdisj})))), + ("c_implies", + (@{const_name implies}, (2, ("fimplies", @{const_name Metis.fimplies})))), + ("equal", + (@{const_name HOL.eq}, (2, ("fequal", @{const_name Metis.fequal}))))] val proxify_const = AList.lookup (op =) metis_proxies #> Option.map snd @@ -140,14 +142,14 @@ (@{const_name Meson.COMBC}, "COMBC"), (@{const_name Meson.COMBS}, "COMBS")] |> Symtab.make - |> fold (Symtab.update o swap o snd o snd) metis_proxies + |> fold (Symtab.update o swap o snd o snd o snd) metis_proxies (* Invert the table of translations between Isabelle and Metis. *) val const_trans_table_inv = const_trans_table |> Symtab.dest |> map swap |> Symtab.make val const_trans_table_unprox = Symtab.empty - |> fold (fn (_, (isa, (_, metis))) => Symtab.update (metis, isa)) + |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa)) metis_proxies val invert_const = perhaps (Symtab.lookup const_trans_table_inv) diff -r 0db96016bdbf -r bd424c3dde46 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:07 2011 +0200 @@ -390,8 +390,7 @@ ATerm (a, us) => if String.isPrefix simple_type_prefix a then @{const True} (* ignore TPTP type information *) - else case strip_prefix_and_unascii const_prefix a of - SOME "equal" => + else if a = tptp_equal then let val ts = map (aux NONE []) us in if length ts = 2 andalso hd ts aconv List.last ts then (* Vampire is keen on producing these. *) @@ -399,7 +398,8 @@ else list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts) end - | SOME s => + else case strip_prefix_and_unascii const_prefix a of + SOME s => let val ((s', s), mangled_us) = s |> unmangled_const |>> `invert_const in @@ -694,11 +694,12 @@ fun repair_name "$true" = "c_True" | repair_name "$false" = "c_False" - | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *) - | repair_name "equal" = "c_equal" (* needed by SPASS? *) + | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) | repair_name s = - if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then - "c_equal" (* seen in Vampire proofs *) + if is_tptp_equal s orelse + (* seen in Vampire proofs *) + (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then + tptp_equal else s diff -r 0db96016bdbf -r bd424c3dde46 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 27 10:30:07 2011 +0200 @@ -342,18 +342,26 @@ let 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)) = + | aux ary top_level (CombConst (name as (s, _), T, T_args)) = (case proxify_const s of - SOME proxy_base => - (* Proxies are not needed in THF, except for partially applied - equality since THF does not provide any syntax for it. *) - if top_level orelse - (is_setting_higher_order format type_sys andalso - (s <> "equal" orelse ary = 2)) then - (case s of - "c_False" => (tptp_false, s') - | "c_True" => (tptp_true, s') - | _ => name, []) + SOME (proxy_ary, proxy_base) => + if top_level orelse is_setting_higher_order format type_sys then + case (top_level, s) of + (_, "c_False") => (`I tptp_false, []) + | (_, "c_True") => (`I tptp_true, []) + | (false, "c_Not") => (`I tptp_not, []) + | (false, "c_conj") => (`I tptp_and, []) + | (false, "c_disj") => (`I tptp_or, []) + | (false, "c_implies") => (`I tptp_implies, []) + | (false, s) => + (* Proxies are not needed in THF, but we generate them for "=" + when it is not fully applied to work around parsing bugs in + the provers ("= @ x @ x" is challenging to some). *) + if is_tptp_equal s andalso ary = proxy_ary then + (`I tptp_equal, []) + else + (proxy_base |>> prefix const_prefix, T_args) + | _ => (name, []) else (proxy_base |>> prefix const_prefix, T_args) | NONE => (name, T_args)) @@ -594,7 +602,8 @@ fact_lift (formula_fold NONE (K (add_combterm_syms_to_table explicit_apply))) val default_sym_table_entries : (string * sym_info) list = - [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}), + [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}), + (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}), (make_fixed_const predicator_name, {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @ ([tptp_false, tptp_true] @@ -751,7 +760,7 @@ fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm]) in Formula (helper_prefix ^ "ti_ti", Axiom, - AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) + AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")])) |> close_formula_universally, simp_info, NONE) end @@ -839,7 +848,7 @@ fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = - accum orelse (s = "equal" andalso member (op =) tms (ATerm (name, []))) + accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false | is_var_nonmonotonic_in_formula pos phi _ name = formula_fold pos (var_occurs_positively_naked_in_term name) phi false @@ -862,7 +871,7 @@ CombConst (name, _, T_args) => (name, T_args) | CombVar (name, _) => (name, []) | CombApp _ => raise Fail "impossible \"CombApp\"" - val arg_site = if site = Top_Level andalso s = "equal" then Eq_Arg + val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg else Elsewhere val t = mk_const_aterm x T_args (map (aux arg_site) args) val T = combtyp_of u @@ -1032,9 +1041,8 @@ out with monotonicity" paper presented at CADE 2011. *) fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I | add_combterm_nonmonotonic_types ctxt level _ - (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1), - tm2)) = - (exists is_var_or_bound_var [tm1, tm2] andalso + (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) = + (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso (case level of Nonmonotonic_Types => not (is_type_surely_infinite ctxt known_infinite_types T) @@ -1117,7 +1125,7 @@ val atomic_Ts = atyps_of T fun eq tms = (if pred_sym then AConn (AIff, map AAtom tms) - else AAtom (ATerm (`I "equal", tms))) + else AAtom (ATerm (`I tptp_equal, tms))) |> bound_atomic_types format type_sys atomic_Ts |> close_formula_universally |> maybe_negate