# HG changeset patch # User blanchet # Date 1307385395 -7200 # Node ID 23b81469499f0269a60f3b8314e42230774635fd # Parent ac02112a208eb281ee18a2efbe1ed0bba24e36f7 more preparations towards hijacking Metis diff -r ac02112a208e -r 23b81469499f src/HOL/Metis_Examples/Proxies.thy --- a/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:36:35 2011 +0200 @@ -24,24 +24,24 @@ lemma "inc \ (\y. 0)" sledgehammer [expect = some] (inc_def plus_1_not_0) -by (metis_eXhaust inc_def plus_1_not_0) +by (new_metis_exhaust inc_def plus_1_not_0) lemma "inc = (\y. y + 1)" sledgehammer [expect = some] (inc_def) -by (metis_eXhaust inc_def) +by (new_metis_exhaust inc_def) definition add_swap :: "nat \ nat \ nat" where "add_swap = (\x y. y + x)" lemma "add_swap m n = n + m" sledgehammer [expect = some] (add_swap_def) -by (metis_eXhaust add_swap_def) +by (new_metis_exhaust add_swap_def) definition "A = {xs\'a list. True}" lemma "xs \ A" sledgehammer [expect = some] -by (metis_eXhaust A_def Collect_def mem_def) +by (new_metis_exhaust A_def Collect_def mem_def) definition "B (y::int) \ y \ 0" definition "C (y::int) \ y \ 1" @@ -51,7 +51,7 @@ lemma "B \ C" sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some] -by (metis_eXhaust B_def C_def int_le_0_imp_le_1 predicate1I) +by (new_metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I) text {* Proxies for logical constants *} @@ -78,7 +78,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "\ id False" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -90,7 +90,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "x = id True \ x = id False" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -102,7 +102,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id x = id True \ id x = id False" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -114,7 +114,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "P True \ P False \ P x" sledgehammer [type_sys = erased, expect = none] () @@ -139,7 +139,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id (\ \ a) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -151,7 +151,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id (\ (id (\ a))) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -163,7 +163,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id (a \ b) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -175,7 +175,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id (a \ b) \ id b" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -187,7 +187,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id a \ id b \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -199,7 +199,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id a \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -211,7 +211,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id b \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -223,7 +223,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id (\ a) \ id (\ b) \ id (\ (a \ b))" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -235,7 +235,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id (\ a) \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -247,7 +247,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) lemma "id (a \ b) \ id (\ a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -259,6 +259,6 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metis_eXhaust id_apply) +by (new_metis_exhaust id_apply) end diff -r ac02112a208e -r 23b81469499f src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Mon Jun 06 20:36:35 2011 +0200 @@ -40,47 +40,47 @@ constr (poly, level, heaviness)) [Preds, Tags]) -fun metis_eXhaust_tac ctxt ths = +fun new_metis_exhaust_tac ctxt ths = let fun tac [] st = all_tac st | tac (type_sys :: type_syss) st = st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *) |> ((if null type_syss then all_tac else rtac @{thm fork} 1) - THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1 + THEN Metis_Tactics.new_metis_tac [type_sys] ctxt ths 1 THEN COND (has_fewer_prems 2) all_tac no_tac THEN tac type_syss) in tac end *} -method_setup metis_eXhaust = {* +method_setup new_metis_exhaust = {* Attrib.thms >> - (fn ths => fn ctxt => SIMPLE_METHOD (metis_eXhaust_tac ctxt ths type_syss)) + (fn ths => fn ctxt => SIMPLE_METHOD (new_metis_exhaust_tac ctxt ths type_syss)) *} "exhaustively run the new Metis with all type encodings" text {* Miscellaneous tests *} lemma "x = y \ y = x" -by metis_eXhaust +by new_metis_exhaust lemma "[a] = [1 + 1] \ a = 1 + (1::int)" -by (metis_eXhaust last.simps) +by (new_metis_exhaust last.simps) lemma "map Suc [0] = [Suc 0]" -by (metis_eXhaust map.simps) +by (new_metis_exhaust map.simps) lemma "map Suc [1 + 1] = [Suc 2]" -by (metis_eXhaust map.simps nat_1_add_1) +by (new_metis_exhaust map.simps nat_1_add_1) lemma "map Suc [2] = [Suc (1 + 1)]" -by (metis_eXhaust map.simps nat_1_add_1) +by (new_metis_exhaust map.simps nat_1_add_1) definition "null xs = (xs = [])" lemma "P (null xs) \ null xs \ xs = []" -by (metis_eXhaust null_def) +by (new_metis_exhaust null_def) lemma "(0::nat) + 0 = 0" -by (metis_eXhaust arithmetic_simps(38)) +by (new_metis_exhaust arithmetic_simps(38)) end diff -r ac02112a208e -r 23b81469499f src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:36:35 2011 +0200 @@ -18,7 +18,7 @@ val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) - fun metis ctxt = Metis_Tactics.metis_tac ctxt (thms @ facts) + fun metis ctxt = Metis_Tactics.new_metis_tac [] ctxt (thms @ facts) in (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |> prefix (metis_tag id) diff -r ac02112a208e -r 23b81469499f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:36:35 2011 +0200 @@ -542,9 +542,9 @@ else if !reconstructor = "smt" then SMT_Solver.smt_tac else if full orelse !reconstructor = "metisFT" then - Metis_Tactics.metisFT_tac + Metis_Tactics.old_metisFT_tac else - Metis_Tactics.metis_tac) ctxt thms + Metis_Tactics.old_metis_tac) ctxt thms fun apply_reconstructor thms = Mirabelle.can_apply timeout (do_reconstructor thms) st diff -r ac02112a208e -r 23b81469499f src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 @@ -230,7 +230,8 @@ fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt - | hol_term_from_metis ctxt MX sym_tab = hol_term_from_metis_MX ctxt sym_tab + | hol_term_from_metis ctxt (Type_Sys _) sym_tab = + hol_term_from_metis_MX ctxt sym_tab fun atp_literal_from_metis (pos, atom) = atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot @@ -514,10 +515,10 @@ 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 = + fun path_finder_fail tm ps t = raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inference, path_finder_" ^ string_of_mode mode ^ - ": path = " ^ space_implode " " (map string_of_int ps) ^ + "equality_inference, path_finder: 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 @@ -542,7 +543,7 @@ 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 = path_finder_fail HO tm ps NONE + | path_finder_HO tm ps = path_finder_fail tm ps NONE fun path_finder_FT tm [] _ = (tm, Bound 0) | path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [t1, _])) = path_finder_FT tm ps t1 @@ -550,7 +551,7 @@ (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 = path_finder_fail FT tm ps (SOME t) + | path_finder_FT tm ps t = path_finder_fail 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)) = let @@ -575,16 +576,16 @@ 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 tm_p = + nth args p' + handle Subscript => path_finder_fail 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) + | path_finder_MX tm ps t = path_finder_fail 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*) @@ -604,7 +605,7 @@ | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 (*if not equality, ignore head to skip the hBOOL predicate*) | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) - | path_finder MX tm ps t = path_finder_MX tm ps t + | path_finder (Type_Sys _) tm ps t = path_finder_MX tm ps t val (tm_subst, body) = path_finder mode i_atom fp m_tm val tm_abs = Abs ("x", type_of tm_subst, body) val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) diff -r ac02112a208e -r 23b81469499f src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200 @@ -9,18 +9,17 @@ signature METIS_TACTICS = sig - type type_sys = ATP_Translate.type_sys - val metisN : string val metisFT_N : string val trace : bool Config.T val verbose : bool Config.T val new_skolemizer : bool Config.T - val metis_tac : Proof.context -> thm list -> int -> tactic - val metisF_tac : Proof.context -> thm list -> int -> tactic - val metisH_tac : Proof.context -> thm list -> int -> tactic - val metisFT_tac : Proof.context -> thm list -> int -> tactic - val metisX_tac : Proof.context -> type_sys option -> thm list -> int -> tactic + val old_metis_tac : Proof.context -> thm list -> int -> tactic + val old_metisF_tac : Proof.context -> thm list -> int -> tactic + val old_metisH_tac : Proof.context -> thm list -> int -> tactic + val old_metisFT_tac : Proof.context -> thm list -> int -> tactic + val new_metis_tac : string list -> Proof.context -> thm list -> int -> tactic + val new_metisFT_tac : Proof.context -> thm list -> int -> tactic val setup : theory -> theory end @@ -31,15 +30,22 @@ open Metis_Translate open Metis_Reconstruct -fun method_binding_for_mode HO = @{binding metis} - | method_binding_for_mode FO = @{binding metisF} - | method_binding_for_mode FT = @{binding metisFT} - | method_binding_for_mode MX = @{binding metisX} +val full_typesN = "full_types" +val default_unsound_type_sys = "poly_args" +val default_sound_type_sys = "poly_preds_query" -val metisN = Binding.qualified_name_of (method_binding_for_mode HO) -val metisF_N = Binding.qualified_name_of (method_binding_for_mode FO) -val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT) -val metisX_N = Binding.qualified_name_of (method_binding_for_mode MX) +fun method_call_for_mode HO = (@{binding metis}, "") + | method_call_for_mode FO = (@{binding metisF}, "") + | method_call_for_mode FT = (@{binding metisFT}, "") + | method_call_for_mode (Type_Sys type_sys) = + if type_sys = default_sound_type_sys then + (@{binding new_metisFT}, "") + else + (@{binding new_metis}, + if type_sys = default_unsound_type_sys then "" else type_sys) + +val metisN = Binding.qualified_name_of @{binding metis} +val metisFT_N = Binding.qualified_name_of @{binding metisFT} val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) @@ -85,7 +91,7 @@ val resolution_params = {active = active_params, waiting = waiting_params} (* Main function to start Metis proof and reconstruction *) -fun FOL_SOLVE type_sys (mode :: fallback_modes) ctxt cls ths0 = +fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt val new_skolemizer = Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) @@ -101,7 +107,7 @@ val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") 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 + prepare_metis_problem ctxt mode cls ths fun get_isa_thm mth Isa_Reflexive_or_Trivial = reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth | get_isa_thm _ (Isa_Raw ith) = ith @@ -167,11 +173,13 @@ (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg else "")) | mode :: _ => - (verbose_warning ctxt - ("Falling back on " ^ - quote (Binding.qualified_name_of - (method_binding_for_mode mode)) ^ "..."); - FOL_SOLVE type_sys fallback_modes ctxt cls ths0) + let val (binding, arg) = method_call_for_mode mode in + (verbose_warning ctxt + ("Falling back on " ^ + quote (Binding.qualified_name_of binding ^ + (arg |> arg <> "" ? enclose " (" ")")) ^ "..."); + FOL_SOLVE fallback_modes ctxt cls ths0) + end val neg_clausify = single @@ -190,12 +198,12 @@ val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) -fun generic_metis_tac modes type_sys ctxt ths i st0 = +fun generic_metis_tac modes ctxt ths i st0 = let val _ = trace_msg ctxt (fn () => "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths)) - fun tac clause = resolve_tac (FOL_SOLVE type_sys modes ctxt clause ths) 1 + fun tac clause = resolve_tac (FOL_SOLVE modes ctxt clause ths) 1 in if exists_type type_has_top_sort (prop_of st0) then (verbose_warning ctxt "Proof state contains the universal sort {}"; @@ -204,17 +212,21 @@ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 end -val metis_modes = [HO, FT] -val metisF_modes = [FO, FT] -val metisH_modes = [HO] -val metisFT_modes = [FT] -val metisX_modes = [MX] +val old_metis_modes = [HO, FT] +val old_metisF_modes = [FO, FT] +val old_metisH_modes = [HO] +val old_metisFT_modes = [FT] +val new_metis_default_modes = + map Type_Sys [default_unsound_type_sys, default_sound_type_sys] +val new_metisFT_modes = [Type_Sys default_sound_type_sys] -val metis_tac = generic_metis_tac metis_modes NONE -val metisF_tac = generic_metis_tac metisF_modes NONE -val metisH_tac = generic_metis_tac metisH_modes NONE -val metisFT_tac = generic_metis_tac metisFT_modes NONE -fun metisX_tac ctxt type_sys = generic_metis_tac metisX_modes type_sys ctxt +val old_metis_tac = generic_metis_tac old_metis_modes +val old_metisF_tac = generic_metis_tac old_metisF_modes +val old_metisH_tac = generic_metis_tac old_metisH_modes +val old_metisFT_tac = generic_metis_tac old_metisFT_modes +fun new_metis_tac [] = generic_metis_tac new_metis_default_modes + | new_metis_tac type_syss = generic_metis_tac (map Type_Sys type_syss) +val new_metisFT_tac = generic_metis_tac new_metisFT_modes (* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. @@ -227,26 +239,30 @@ fun method modes (type_sys, ths) ctxt facts = let val (schem_facts, nonschem_facts) = List.partition has_tvar facts - val type_sys = type_sys |> Option.map type_sys_from_string + val modes = type_sys |> Option.map (single o Type_Sys) |> the_default modes in HEADGOAL (Method.insert_tac nonschem_facts THEN' - CHANGED_PROP - o generic_metis_tac modes type_sys ctxt (schem_facts @ ths)) + CHANGED_PROP o generic_metis_tac modes ctxt (schem_facts @ ths)) end fun setup_method (modes as mode :: _) = - Method.setup (method_binding_for_mode mode) - ((if mode = MX then - Scan.lift (Scan.option (Args.parens Parse.short_ident)) - else - Scan.succeed NONE) - -- Attrib.thms >> (METHOD oo method modes)) + (if modes = new_metis_default_modes then + (Args.parens Parse.short_ident + >> (fn s => if s = full_typesN then default_sound_type_sys else s)) + |> Scan.option |> Scan.lift + else + Scan.succeed NONE) + -- Attrib.thms >> (METHOD oo method modes) + |> Method.setup (fst (method_call_for_mode mode)) val setup = - [(metis_modes, "Metis for FOL and HOL problems"), - (metisF_modes, "Metis for FOL problems"), - (metisFT_modes, "Metis for FOL/HOL problems with fully-typed translation"), - (metisX_modes, "Metis for FOL and HOL problems (experimental)")] + [(old_metis_modes, "Metis for FOL and HOL problems"), + (old_metisF_modes, "Metis for FOL problems (legacy)"), + (old_metisFT_modes, + "Metis for FOL/HOL problems with fully-typed translation"), + (new_metis_default_modes, "Metis for FOL and HOL problems (experimental)"), + (new_metisFT_modes, + "Metis for FOL/HOL problems with fully-typed translation (experimental)")] |> fold (uncurry setup_method) end; diff -r ac02112a208e -r 23b81469499f src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200 @@ -10,9 +10,8 @@ signature METIS_TRANSLATE = sig type type_literal = ATP_Translate.type_literal - type type_sys = ATP_Translate.type_sys - datatype mode = FO | HO | FT | MX + datatype mode = FO | HO | FT | Type_Sys of string datatype isa_thm = Isa_Reflexive_or_Trivial | @@ -32,7 +31,7 @@ val reveal_old_skolem_terms : (string * term) list -> term -> term val string_of_mode : mode -> string val prepare_metis_problem : - Proof.context -> mode -> type_sys option -> thm list -> thm list + Proof.context -> mode -> thm list -> thm list -> mode * int Symtab.table * metis_problem end @@ -118,13 +117,13 @@ (* HOL to FOL (Isabelle to Metis) *) (* ------------------------------------------------------------------------- *) -(* first-order, higher-order, fully-typed, mode X (fleXible) *) -datatype mode = FO | HO | FT | MX +(* first-order, higher-order, fully-typed, ATP type system *) +datatype mode = FO | HO | FT | Type_Sys of string fun string_of_mode FO = "FO" | string_of_mode HO = "HO" | string_of_mode FT = "FT" - | string_of_mode MX = "MX" + | string_of_mode (Type_Sys type_sys) = "Type_Sys " ^ type_sys fun fn_isa_to_met_sublevel "equal" = "c_fequal" | fn_isa_to_met_sublevel "c_False" = "c_fFalse" @@ -346,13 +345,11 @@ end | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" -(* FIXME: put in "Metis_Tactics" as string *) -val default_type_sys = Preds (Polymorphic, Const_Arg_Types, Lightweight) - (* Function to generate metis clauses, including comb and type clauses *) -fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses = +fun prepare_metis_problem ctxt (mode as Type_Sys type_sys) conj_clauses + fact_clauses = let - val type_sys = type_sys |> the_default default_type_sys + val type_sys = type_sys_from_string type_sys val explicit_apply = NONE val clauses = conj_clauses @ fact_clauses @@ -382,9 +379,9 @@ val axioms = atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) in - (MX, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems}) + (mode, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems}) end - | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses = + | prepare_metis_problem ctxt mode conj_clauses fact_clauses = let val thy = Proof_Context.theory_of ctxt (* The modes FO and FT are sticky. HO can be downgraded to FO. *) diff -r ac02112a208e -r 23b81469499f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:35 2011 +0200 @@ -416,8 +416,8 @@ val full_tac = Method.insert_tac facts i THEN tac ctxt i in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end -fun tac_for_reconstructor Metis = Metis_Tactics.metisH_tac - | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac +fun tac_for_reconstructor Metis = Metis_Tactics.old_metisH_tac + | tac_for_reconstructor MetisFT = Metis_Tactics.old_metisFT_tac | tac_for_reconstructor _ = raise Fail "unexpected reconstructor" fun timed_reconstructor reconstructor debug timeout ths = diff -r ac02112a208e -r 23b81469499f src/HOL/ex/CASC_Setup.thy --- a/src/HOL/ex/CASC_Setup.thy Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/ex/CASC_Setup.thy Mon Jun 06 20:36:35 2011 +0200 @@ -51,7 +51,8 @@ SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) ORELSE - SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt [])) + SOLVE_TIMEOUT (max_secs div 10) "metis" + (ALLGOALS (Metis_Tactics.new_metis_tac ctxt NONE [])) ORELSE SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) ORELSE diff -r ac02112a208e -r 23b81469499f src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Mon Jun 06 20:36:35 2011 +0200 @@ -70,7 +70,7 @@ in case run_atp false timeout i i ctxt th atp of SOME facts => - Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th + Metis_Tactics.new_metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th | NONE => Seq.empty end