# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID 81d1b15aa0aed3ddb4826a3a55feca0ee0248395 # Parent 35962353e36b067528d49c7188221ca9b60fc95b use ":" for type information (looks good in Metis's output) and handle it in new path finder diff -r 35962353e36b -r 81d1b15aa0ae src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -52,7 +52,6 @@ type translated_formula - val type_tag_name : string val bound_var_prefix : string val schematic_var_prefix: string val fixed_var_prefix: string @@ -70,6 +69,7 @@ val typed_helper_suffix : string val predicator_name : string val app_op_name : string + val type_tag_name : string val type_pred_name : string val simple_type_prefix : string val ascii_of: string -> string @@ -146,8 +146,6 @@ val elim_info = useful_isabelle_info "elim" val simp_info = useful_isabelle_info "simp" -val type_tag_name = "ti" - val bound_var_prefix = "B_" val schematic_var_prefix = "V_" val fixed_var_prefix = "v_" @@ -178,6 +176,7 @@ val predicator_name = "hBOOL" val app_op_name = "hAPP" +val type_tag_name = "ti" val type_pred_name = "is" val simple_type_prefix = "ty_" diff -r 35962353e36b -r 81d1b15aa0ae src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200 @@ -180,20 +180,20 @@ else Const (c, dummyT) end - fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = + fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) = (case strip_prefix_and_unascii schematic_var_prefix v of SOME w => mk_var(w, dummyT) | NONE => mk_var(v, dummyT)) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) = + | cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) = Const (@{const_name HOL.eq}, HOLogic.typeT) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = + | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) = (case strip_prefix_and_unascii const_prefix x of SOME c => do_const c | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix_and_unascii fixed_var_prefix x of SOME v => Free (v, hol_type_from_metis_term ctxt ty) | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".", [tm1,tm2]), _])) = + | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (".", [tm1,tm2]), _])) = cvt tm1 $ cvt tm2 | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) cvt tm1 $ cvt tm2 @@ -215,11 +215,13 @@ in fol_tm |> cvt end fun atp_name_from_metis s = - case AList.find (op =) metis_name_table s of - (s', ary) :: _ => (s', SOME ary) - | _ => (s, NONE) + case find_first (fn (_, (s', _)) => s' = s) metis_name_table of + SOME ((s, _), (_, swap)) => (s, swap) + | _ => (s, false) fun atp_term_from_metis (Metis_Term.Fn (s, tms)) = - ATerm (fst (atp_name_from_metis s), map atp_term_from_metis tms) + let val (s, swap) = atp_name_from_metis s in + ATerm (s, tms |> map atp_term_from_metis |> swap ? rev) + end | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, []) fun hol_term_from_metis_MX sym_tab ctxt = @@ -487,6 +489,14 @@ val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) fun replace_item_list lx 0 (_::ls) = lx::ls | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls + fun path_finder_fail mode tm ps t = + raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ + "equality_inf, path_finder_" ^ string_of_mode mode ^ + ": path = " ^ space_implode " " (map string_of_int ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm ^ + (case t of + SOME t => " fol-term: " ^ Metis_Term.toString t + | NONE => "")) fun path_finder_FO tm [] = (tm, Bound 0) | path_finder_FO tm (p::ps) = let val (tm1,args) = strip_comb tm @@ -507,27 +517,22 @@ fun path_finder_HO tm [] = (tm, Bound 0) | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) - | path_finder_HO tm ps = - raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf, path_finder_HO: path = " ^ - space_implode " " (map string_of_int ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm) + | path_finder_HO tm ps = path_finder_fail HO tm ps NONE fun path_finder_FT tm [] _ = (tm, Bound 0) - | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = + | path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [t1, _])) = path_finder_FT tm ps t1 | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) - | path_finder_FT tm ps t = - raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf, path_finder_FT: path = " ^ - space_implode " " (map string_of_int ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm ^ - " fol-term: " ^ Metis_Term.toString t) + | 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)) = - if s = metis_app_op (* FIXME ### mangled etc. *) then + (* FIXME ### what if these are mangled? *) + if s = metis_type_tag then + if p = 1 then path_finder_MX tm ps (nth ts 1) + 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) @@ -540,21 +545,13 @@ val p' = if adjustment > p then p else p - adjustment val tm_p = nth args p' handle Subscript => - raise METIS ("equality_inf", - string_of_int p ^ " adj " ^ - string_of_int adjustment ^ " term " ^ - Syntax.string_of_term ctxt tm) + 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 - | path_finder_MX tm ps t = - raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf, path_finder_MX: path = " ^ - space_implode " " (map string_of_int ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm ^ - " fol-term: " ^ Metis_Term.toString t) + | 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) _ = (*equality: not curried, as other predicates are*) diff -r 35962353e36b -r 81d1b15aa0ae src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -20,10 +20,11 @@ old_skolems : (string * term) list} val metis_equal : string + val metis_type_tag : string val metis_predicator : string val metis_app_op : string val metis_generated_var_prefix : string - val metis_name_table : ((string * int) * string) list + val metis_name_table : ((string * int) * (string * bool)) list val reveal_old_skolem_terms : (string * term) list -> term -> term val string_of_mode : mode -> string val prepare_metis_problem : @@ -40,13 +41,15 @@ val metis_equal = "=" val metis_predicator = "{}" val metis_app_op = "." +val metis_type_tag = ":" val metis_generated_var_prefix = "_" val metis_name_table = - [((tptp_equal, 2), metis_equal), - ((tptp_old_equal, 2), metis_equal), - ((const_prefix ^ predicator_name, 1), metis_predicator), - ((const_prefix ^ app_op_name, 2), metis_app_op)] + [((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))] fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) | predicate_of thy (t, pos) = @@ -160,7 +163,7 @@ (*The fully-typed translation, to avoid type errors*) fun tag_with_type tm T = - Metis_Term.Fn (type_tag_name, [tm, metis_term_from_typ T]) + Metis_Term.Fn (metis_type_tag, [tm, metis_term_from_typ T]) fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = tag_with_type (Metis_Term.Var s) ty @@ -283,15 +286,18 @@ in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end fun metis_name_from_atp s ary = - AList.lookup (op =) metis_name_table (s, ary) |> the_default s + AList.lookup (op =) metis_name_table (s, ary) |> the_default (s, false) fun metis_term_from_atp (ATerm (s, tms)) = if is_tptp_variable s then Metis_Term.Var s else - Metis_Term.Fn (metis_name_from_atp s (length tms), - map metis_term_from_atp tms) -fun metis_atom_from_atp (AAtom (ATerm (s, tms))) = - (metis_name_from_atp s (length tms), map metis_term_from_atp tms) + let val (s, swap) = metis_name_from_atp s (length tms) in + Metis_Term.Fn (s, tms |> map metis_term_from_atp |> swap ? rev) + end +fun metis_atom_from_atp (AAtom tm) = + (case metis_term_from_atp tm of + Metis_Term.Fn x => x + | _ => raise Fail "non CNF -- expected function") | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom" fun metis_literal_from_atp (AConn (ANot, [phi])) = (false, metis_atom_from_atp phi)