# HG changeset patch # User blanchet # Date 1306916983 -7200 # Node ID 4301f1c123d6e0b5b009462cc807840228c5f327 # Parent a198260805967fae70bfed37d59b9aa759204eb2 support lightweight tags in new Metis diff -r a19826080596 -r 4301f1c123d6 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 @@ -66,7 +66,7 @@ val type_decl_prefix : string val sym_decl_prefix : string val preds_sym_formula_prefix : string - val tags_sym_formula_prefix : string + val lightweight_tags_sym_formula_prefix : string val fact_prefix : string val conjecture_prefix : string val helper_prefix : string @@ -172,7 +172,7 @@ val type_decl_prefix = "ty_" val sym_decl_prefix = "sy_" val preds_sym_formula_prefix = "psy_" -val tags_sym_formula_prefix = "tsy_" +val lightweight_tags_sym_formula_prefix = "tsy_" val fact_prefix = "fact_" val conjecture_prefix = "conj_" val helper_prefix = "help_" @@ -1665,11 +1665,11 @@ intro_info, NONE) end -fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind nonmono_Ts - type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = +fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind + nonmono_Ts type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = let val ident_base = - tags_sym_formula_prefix ^ s ^ + lightweight_tags_sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "") val (kind, maybe_negate) = if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) @@ -1749,8 +1749,8 @@ | Lightweight => let val n = length decls in (0 upto n - 1 ~~ decls) - |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind - nonmono_Ts type_sys n s) + |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format + conj_sym_kind nonmono_Ts type_sys n s) end) fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts diff -r a19826080596 -r 4301f1c123d6 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Wed Jun 01 10:29:43 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Wed Jun 01 10:29:43 2011 +0200 @@ -55,6 +55,28 @@ fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) | used_axioms _ _ = NONE +fun cterm_from_metis ctxt sym_tab tm = + let val thy = Proof_Context.theory_of ctxt in + tm |> hol_term_from_metis MX sym_tab ctxt + |> Syntax.check_term + (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) + |> cterm_of thy + end + +(* Lightweight predicate type information comes in two flavors, "t = t'" and + "t => t'", where "t" and "t'" are the same term modulo type tags. + In Isabelle, type tags are stripped away, so we are left with "t = t" or + "t => t". *) +fun lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth = + (case Metis_LiteralSet.toList (Metis_Thm.clause mth) of + [(true, (_, [_, tm]))] => + tm |> cterm_from_metis ctxt sym_tab |> Thm.reflexive + RS @{thm meta_eq_to_obj_eq} + | [_, (_, tm)] => + tm |> Metis_Term.Fn |> cterm_from_metis ctxt sym_tab |> Thm.assume + | _ => raise Fail "unexpected tags sym clause") + |> Meson.make_meta_clause + val clause_params = {ordering = Metis_KnuthBendixOrder.default, orderLiterals = Metis_Clause.UnsignedLiteralOrder, @@ -88,6 +110,11 @@ val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths val (mode, sym_tab, {axioms, old_skolems, ...}) = prepare_metis_problem ctxt mode type_sys cls ths + val axioms = + axioms |> map + (fn (mth, SOME th) => (mth, th) + | (mth, NONE) => + (mth, lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth)) val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") val thms = map #1 axioms val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms diff -r a19826080596 -r 4301f1c123d6 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 @@ -15,7 +15,7 @@ datatype mode = FO | HO | FT | MX type metis_problem = - {axioms : (Metis_Thm.thm * thm) list, + {axioms : (Metis_Thm.thm * thm option) list, tfrees : type_literal list, old_skolems : (string * term) list} @@ -236,7 +236,7 @@ (* ------------------------------------------------------------------------- *) type metis_problem = - {axioms : (Metis_Thm.thm * thm) list, + {axioms : (Metis_Thm.thm * thm option) list, tfrees : type_literal list, old_skolems : (string * term) list} @@ -309,14 +309,17 @@ (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList |> Metis_Thm.axiom, case try (unprefix conjecture_prefix) ident of - SOME s => Meson.make_meta_clause (nth clauses (the (Int.fromString s))) + SOME s => + SOME (Meson.make_meta_clause (nth clauses (the (Int.fromString s)))) | NONE => + if String.isPrefix lightweight_tags_sym_formula_prefix ident then + NONE (* FIXME: missing: - if String.isPrefix helper_prefix then + else if String.isPrefix helper_prefix then ... +*) else -*) - TrueI) + SOME TrueI) | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight) @@ -363,15 +366,15 @@ hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems metis_ith in - {axioms = (mth, isa_ith) :: axioms, + {axioms = (mth, SOME isa_ith) :: axioms, tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} end; fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} = - {axioms = (mth, ith) :: axioms, tfrees = tfrees, + {axioms = (mth, SOME ith) :: axioms, tfrees = tfrees, old_skolems = old_skolems} fun add_tfrees {axioms, tfrees, old_skolems} = - {axioms = - map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ axioms, + {axioms = map (rpair (SOME TrueI) o metis_of_tfree) + (distinct (op =) tfrees) @ axioms, tfrees = tfrees, old_skolems = old_skolems} val problem = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}