cleaner handling of equality and proxies (esp. for THF)
--- 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
--- 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)
--- 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
--- 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