--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200
@@ -450,7 +450,7 @@
else if s' = predicator_name then
do_term [] (SOME @{typ bool}) (hd us)
else if s' = app_op_name then
- do_term (nth us 1 :: extra_us) opt_T (hd us)
+ do_term (List.last us :: extra_us) opt_T (nth us (length us - 2))
else if s' = type_pred_name then
@{const True} (* ignore type predicates *)
else
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 01 10:29:43 2011 +0200
@@ -80,6 +80,8 @@
val type_tag_name : string
val type_pred_name : string
val simple_type_prefix : string
+ val prefixed_app_op_name : string
+ val prefixed_type_tag_name : string
val ascii_of: string -> string
val unascii_of: string -> string
val strip_prefix_and_unascii : string -> string -> string option
@@ -113,6 +115,7 @@
val is_type_sys_fairly_sound : type_sys -> bool
val choose_format : format list -> type_sys -> format * type_sys
val raw_type_literals_for_types : typ list -> type_literal list
+ val unmangled_const_name : string -> string
val unmangled_const : string -> string * string fo_term list
val translate_atp_fact :
Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
@@ -189,6 +192,9 @@
val type_pred_name = "is"
val simple_type_prefix = "ty_"
+val prefixed_app_op_name = const_prefix ^ app_op_name
+val prefixed_type_tag_name = const_prefix ^ type_tag_name
+
(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"
@@ -1138,13 +1144,14 @@
fun list_app head args = fold (curry (CombApp o swap)) args head
+val app_op = `make_fixed_const app_op_name
+
fun explicit_app arg head =
let
val head_T = combtyp_of head
val (arg_T, res_T) = dest_funT head_T
val explicit_app =
- CombConst (`make_fixed_const app_op_name, head_T --> head_T,
- [arg_T, res_T])
+ CombConst (app_op, head_T --> head_T, [arg_T, res_T])
in list_app explicit_app [head, arg] end
fun list_explicit_app head args = fold explicit_app args head
@@ -1201,8 +1208,7 @@
anyway, by distinguishing overloads only on the homogenized
result type. Don't do it for lightweight type systems, though,
since it leads to too many unsound proofs. *)
- if s = const_prefix ^ app_op_name andalso
- length T_args = 2 andalso
+ if s = prefixed_app_op_name andalso length T_args = 2 andalso
not (is_type_sys_virtually_sound type_sys) andalso
heaviness_of_type_sys type_sys = Heavyweight then
T_args |> map (homogenized_type ctxt nonmono_Ts level 0)
@@ -1277,10 +1283,12 @@
by (unfold fimplies_def) fast+})),
("If", (true, @{thms if_True if_False True_or_False}))]
+val type_tag = `make_fixed_const type_tag_name
+
fun ti_ti_helper_fact () =
let
fun var s = ATerm (`I s, [])
- fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
+ fun tag tm = ATerm (type_tag, [var "X", tm])
in
Formula (helper_prefix ^ "ti_ti", Axiom,
AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))
@@ -1402,8 +1410,10 @@
fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
+val type_pred = `make_fixed_const type_pred_name
+
fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =
- CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T])
+ CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
|> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
tm)
@@ -1418,7 +1428,7 @@
ATerm (x, map (fo_term_from_typ false) T_args @ args)
fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
- CombConst (`make_fixed_const type_tag_name, T --> T, [T])
+ CombConst (type_tag, T --> T, [T])
|> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
|> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200
@@ -530,29 +530,33 @@
| path_finder_FT tm ps t = path_finder_fail FT tm ps (SOME t)
fun path_finder_MX tm [] _ = (tm, Bound 0)
| path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
- (* FIXME ### what if these are mangled? *)
- if s = metis_type_tag then
- if p = 0 then path_finder_MX tm ps (hd ts)
- else path_finder_fail MX tm (p :: ps) (SOME t)
- else if s = metis_app_op then
- let
- val (tm1, tm2) = dest_comb tm in
- if p = 0 then path_finder_MX tm1 ps (hd ts) ||> (fn y => y $ tm2)
- else path_finder_MX tm2 ps (nth ts 1) ||> (fn y => tm1 $ y)
- end
- else
- let
- val (tm1, args) = strip_comb tm
- val adjustment = length ts - length args
- val p' = if adjustment > p then p else p - adjustment
- val tm_p = nth args p'
- handle Subscript =>
- path_finder_fail MX tm (p :: ps) (SOME t)
- val _ = trace_msg ctxt (fn () =>
- "path_finder: " ^ string_of_int p ^ " " ^
- Syntax.string_of_term ctxt tm_p)
- val (r, t) = path_finder_MX tm_p ps (nth ts p)
- in (r, list_comb (tm1, replace_item_list t p' args)) end
+ let val s = s |> unmangled_const_name in
+ if s = metis_type_tag orelse s = prefixed_type_tag_name then
+ path_finder_MX tm ps (nth ts p)
+ else if s = metis_app_op orelse s = prefixed_app_op_name then
+ let
+ val (tm1, tm2) = dest_comb tm
+ val p' = p - (length ts - 2)
+ in
+ if p' = 0 then
+ path_finder_MX tm1 ps (nth ts p) ||> (fn y => y $ tm2)
+ else
+ path_finder_MX tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
+ end
+ else
+ let
+ val (tm1, args) = strip_comb tm
+ val adjustment = length ts - length args
+ val p' = if adjustment > p then p else p - adjustment
+ val tm_p = nth args p'
+ handle Subscript =>
+ path_finder_fail MX tm (p :: ps) (SOME t)
+ val _ = trace_msg ctxt (fn () =>
+ "path_finder: " ^ string_of_int p ^ " " ^
+ Syntax.string_of_term ctxt tm_p)
+ val (r, t) = path_finder_MX tm_p ps (nth ts p)
+ in (r, list_comb (tm1, replace_item_list t p' args)) end
+ end
| path_finder_MX tm ps t = path_finder_fail MX tm ps (SOME t)
fun path_finder FO tm ps _ = path_finder_FO tm ps
| path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 01 10:29:43 2011 +0200
@@ -48,8 +48,8 @@
[((tptp_equal, 2), (metis_equal, false)),
((tptp_old_equal, 2), (metis_equal, false)),
((const_prefix ^ predicator_name, 1), (metis_predicator, false)),
- ((const_prefix ^ app_op_name, 2), (metis_app_op, false)),
- ((const_prefix ^ type_tag_name, 2), (metis_type_tag, true))]
+ ((prefixed_app_op_name, 2), (metis_app_op, false)),
+ ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
| predicate_of thy (t, pos) =