# HG changeset patch # User blanchet # Date 1306916983 -7200 # Node ID d73fc2e553085ada2a6fa7418d6bd84a449da57e # Parent 4301f1c123d6e0b5b009462cc807840228c5f327 implemented missing hAPP and ti cases of new path finder diff -r 4301f1c123d6 -r d73fc2e55308 src/HOL/Tools/ATP/atp_reconstruct.ML --- 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 diff -r 4301f1c123d6 -r d73fc2e55308 src/HOL/Tools/ATP/atp_translate.ML --- 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])) diff -r 4301f1c123d6 -r d73fc2e55308 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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) _ = diff -r 4301f1c123d6 -r d73fc2e55308 src/HOL/Tools/Metis/metis_translate.ML --- 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) =