# HG changeset patch # User blanchet # Date 1321432947 -3600 # Node ID 973bb7846505d06ac74810b3f9ab7632a8ec25e5 # Parent 25388cf064370620321f9a9a88eb5a4e17152110 parse lambda translation option in Metis diff -r 25388cf06437 -r 973bb7846505 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 15 22:20:58 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 16 09:42:27 2011 +0100 @@ -11,7 +11,7 @@ val type_encK = "type_enc" val soundK = "sound" val slicingK = "slicing" -val lambda_transK = "lambda_trans" +val lam_transK = "lam_trans" val e_weight_methodK = "e_weight_method" val force_sosK = "force_sos" val max_relevantK = "max_relevant" @@ -355,7 +355,7 @@ SH_FAIL of int * int | SH_ERROR -fun run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans +fun run_sh prover_name prover type_enc sound max_relevant slicing lam_trans e_weight_method force_sos hard_timeout timeout dir pos st = let val {context = ctxt, facts = chained_ths, goal} = Proof.goal st @@ -371,9 +371,6 @@ val st' = st |> Proof.map_context (set_file_name dir - #> (Option.map (Config.put - Sledgehammer_Provers.atp_lambda_trans) - lambda_trans |> the_default I) #> (Option.map (Config.put ATP_Systems.e_weight_method) e_weight_method |> the_default I) #> (Option.map (Config.put ATP_Systems.force_sos) @@ -383,6 +380,7 @@ [("verbose", "true"), ("type_enc", type_enc), ("sound", sound), + ("lam_trans", lam_trans |> the_default "smart"), ("preplay_timeout", preplay_timeout), ("max_relevant", max_relevant), ("slicing", slicing), @@ -465,7 +463,7 @@ val sound = AList.lookup (op =) args soundK |> the_default "false" val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart" val slicing = AList.lookup (op =) args slicingK |> the_default "true" - val lambda_trans = AList.lookup (op =) args lambda_transK + val lam_trans = AList.lookup (op =) args lam_transK val e_weight_method = AList.lookup (op =) args e_weight_methodK val force_sos = AList.lookup (op =) args force_sosK |> Option.map (curry (op <>) "false") @@ -475,7 +473,7 @@ minimizer has a chance to do its magic *) val hard_timeout = SOME (2 * timeout) val (msg, result) = - run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans + run_sh prover_name prover type_enc sound max_relevant slicing lam_trans e_weight_method force_sos hard_timeout timeout dir pos st in case result of @@ -576,15 +574,17 @@ ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??" ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??" ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags" - ORELSE' Metis_Tactic.metis_tac [] ctxt thms + ORELSE' Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms else if !reconstructor = "smt" then SMT_Solver.smt_tac ctxt thms else if full orelse !reconstructor = "metis (full_types)" then - Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc] ctxt thms + Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc] + ATP_Translate.combinatorsN ctxt thms else if !reconstructor = "metis (no_types)" then - Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] ctxt thms + Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] + ATP_Translate.combinatorsN ctxt thms else if !reconstructor = "metis" then - Metis_Tactic.metis_tac [] ctxt thms + Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms else K all_tac end diff -r 25388cf06437 -r 973bb7846505 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 15 22:20:58 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Nov 16 09:42:27 2011 +0100 @@ -90,13 +90,13 @@ val is_type_enc_fairly_sound : type_enc -> bool val type_enc_from_string : soundness -> string -> type_enc val adjust_type_enc : atp_format -> type_enc -> type_enc - val lift_lambdas : - Proof.context -> type_enc -> term list -> term list * term list val mk_aconns : connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula val unmangled_const : string -> string * (string, 'b) ho_term list val unmangled_const_name : string -> string val helper_table : ((string * bool) * thm list) list + val trans_lams_from_string : + Proof.context -> type_enc -> string -> term list -> term list * term list val factsN : string val prepare_atp_problem : Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc @@ -690,7 +690,7 @@ open_form (subst_bound (Var ((s, 0), T), t)) | open_form t = t -fun lift_lambdas ctxt type_enc = +fun lift_lams ctxt type_enc = map (Envir.eta_contract #> close_form) #> rpair ctxt #-> Lambda_Lifting.lift_lambdas (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then @@ -1165,10 +1165,10 @@ handle THM _ => t |> do_cheaply_conceal_lambdas Ts val introduce_combinators = simple_translate_lambdas do_introduce_combinators -fun preprocess_abstractions_in_terms trans_lambdas facts = +fun preprocess_abstractions_in_terms trans_lams facts = let val (facts, lambda_ts) = - facts |> map (snd o snd) |> trans_lambdas + facts |> map (snd o snd) |> trans_lams |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts val lambda_facts = map2 (fn t => fn j => @@ -1677,28 +1677,28 @@ end | extract_lambda_def _ = raise Fail "malformed lifted lambda" -fun translate_formulas ctxt format prem_kind type_enc lambda_trans presimp - hyp_ts concl_t facts = +fun trans_lams_from_string ctxt type_enc lam_trans = + if lam_trans = no_lamsN then + rpair [] + else if lam_trans = hide_lamsN then + lift_lams ctxt type_enc ##> K [] + else if lam_trans = lam_liftingN then + lift_lams ctxt type_enc + else if lam_trans = combinatorsN then + map (introduce_combinators ctxt) #> rpair [] + else if lam_trans = hybrid_lamsN then + lift_lams ctxt type_enc + ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)]) + else if lam_trans = keep_lamsN then + map (Envir.eta_contract) #> rpair [] + else + error ("Unknown lambda translation method: " ^ quote lam_trans ^ ".") + +fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts + concl_t facts = let val thy = Proof_Context.theory_of ctxt - val trans_lambdas = - if lambda_trans = no_lamsN then - rpair [] - else if lambda_trans = hide_lamsN then - lift_lambdas ctxt type_enc ##> K [] - else if lambda_trans = lam_liftingN then - lift_lambdas ctxt type_enc - else if lambda_trans = combinatorsN then - map (introduce_combinators ctxt) #> rpair [] - else if lambda_trans = hybrid_lamsN then - lift_lambdas ctxt type_enc - ##> maps (fn t => [t, introduce_combinators ctxt - (intentionalize_def t)]) - else if lambda_trans = keep_lamsN then - map (Envir.eta_contract) #> rpair [] - else - error ("Unknown lambda translation method: " ^ - quote lambda_trans ^ ".") + val trans_lams = trans_lams_from_string ctxt type_enc lam_trans val presimp_consts = Meson.presimplified_consts ctxt val fact_ts = facts |> map snd (* Remove existing facts from the conjecture, as this can dramatically @@ -1715,11 +1715,11 @@ (conjs, facts) |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))) - |> (if lambda_trans = no_lamsN then + |> (if lam_trans = no_lamsN then rpair [] else op @ - #> preprocess_abstractions_in_terms trans_lambdas + #> preprocess_abstractions_in_terms trans_lams #>> chop (length conjs)) val conjs = conjs |> make_conjecture ctxt format type_enc val (fact_names, facts) = @@ -2330,7 +2330,7 @@ val explicit_apply_threshold = 50 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter - lambda_trans readable_names preproc hyp_ts concl_t facts = + lam_trans readable_names preproc hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt val type_enc = type_enc |> adjust_type_enc format @@ -2343,19 +2343,19 @@ NONE else SOME false - val lambda_trans = - if lambda_trans = smartN then + val lam_trans = + if lam_trans = smartN then if is_type_enc_higher_order type_enc then keep_lamsN else combinatorsN - else if lambda_trans = keep_lamsN andalso + else if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then error ("Lambda translation method incompatible with first-order \ \encoding.") else - lambda_trans + lam_trans val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses, lifted) = - translate_formulas ctxt format prem_kind type_enc lambda_trans preproc - hyp_ts concl_t facts + translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts + concl_t facts val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc diff -r 25388cf06437 -r 973bb7846505 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:20:58 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Wed Nov 16 09:42:27 2011 +0100 @@ -23,7 +23,8 @@ val verbose : bool Config.T val new_skolemizer : bool Config.T val type_has_top_sort : typ -> bool - val metis_tac : string list -> Proof.context -> thm list -> int -> tactic + val metis_tac : + string list -> string -> Proof.context -> thm list -> int -> tactic val setup : theory -> theory end @@ -53,11 +54,15 @@ (partial_typesN, partial_type_syss), (no_typesN, [no_type_enc])] -fun method_call_for_type_enc type_syss = +val lam_transs = [hide_lamsN, lam_liftingN, combinatorsN] +val default_lam_trans = combinatorsN + +fun method_call_for type_syss lam_trans = metisN ^ " (" ^ (case AList.find (op =) type_enc_aliases type_syss of [alias] => alias - | _ => hd type_syss) ^ ")" + | _ => hd type_syss) ^ + (if lam_trans = default_lam_trans then "" else ", " ^ lam_trans) ^ ")" val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) @@ -130,7 +135,7 @@ val resolution_params = {active = active_params, waiting = waiting_params} (* Main function to start Metis proof and reconstruction *) -fun FOL_SOLVE (type_enc :: fallback_type_syss) lambda_trans ctxt cls ths0 = +fun FOL_SOLVE (type_enc :: fallback_type_syss) lam_trans 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) @@ -138,7 +143,7 @@ map2 (fn j => fn th => (Thm.get_name_hint th, Meson_Clausify.cnf_axiom ctxt new_skolemizer - (lambda_trans = combinatorsN) j th)) + (lam_trans = combinatorsN) j th)) (0 upto length ths0 - 1) ths0 val ths = maps (snd o snd) th_cls_pairs val dischargers = map (fst o snd) th_cls_pairs @@ -147,13 +152,13 @@ val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) val type_enc = type_enc_from_string Sound type_enc val (sym_tab, axioms, concealed) = - prepare_metis_problem ctxt type_enc lambda_trans cls ths + prepare_metis_problem ctxt type_enc lam_trans cls ths fun get_isa_thm mth Isa_Reflexive_or_Trivial = reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth | get_isa_thm mth Isa_Lambda_Lifted = lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth | get_isa_thm _ (Isa_Raw ith) = - ith |> lambda_trans = lam_liftingN + ith |> lam_trans = lam_liftingN ? introduce_lambda_wrappers_in_theorem ctxt val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") @@ -221,8 +226,8 @@ | _ => (verbose_warning ctxt ("Falling back on " ^ - quote (method_call_for_type_enc fallback_type_syss) ^ "..."); - FOL_SOLVE fallback_type_syss lambda_trans ctxt cls ths0) + quote (method_call_for fallback_type_syss lam_trans) ^ "..."); + FOL_SOLVE fallback_type_syss lam_trans ctxt cls ths0) fun neg_clausify ctxt combinators = single @@ -241,21 +246,20 @@ val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) -fun generic_metis_tac type_syss ctxt ths i st0 = +fun generic_metis_tac type_syss lam_trans ctxt ths i st0 = let - val lambda_trans = Config.get ctxt lambda_trans 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_syss lambda_trans ctxt clause ths) 1 + resolve_tac (FOL_SOLVE type_syss lam_trans 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 {}" else (); Meson.MESON (preskolem_tac ctxt) - (maps (neg_clausify ctxt (lambda_trans = combinatorsN))) tac ctxt i st0 + (maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0 end fun metis_tac [] = generic_metis_tac partial_type_syss @@ -269,7 +273,7 @@ val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of -fun method default_type_syss (override_type_syss, ths) ctxt facts = +fun method default_type_syss ((override_type_syss, lam_trans), ths) ctxt facts = let val _ = if default_type_syss = full_type_syss then @@ -278,16 +282,28 @@ () val (schem_facts, nonschem_facts) = List.partition has_tvar facts val type_syss = override_type_syss |> the_default default_type_syss + val lam_trans = lam_trans |> the_default default_lam_trans in HEADGOAL (Method.insert_tac nonschem_facts THEN' - CHANGED_PROP - o generic_metis_tac type_syss ctxt (schem_facts @ ths)) + CHANGED_PROP o generic_metis_tac type_syss lam_trans ctxt + (schem_facts @ ths)) end +fun consider_arg s = + if member (op =) lam_transs s then + apsnd (K (SOME s)) + else + apfst (K (SOME (AList.lookup (op =) type_enc_aliases s |> the_default [s]))) + fun setup_method (binding, type_syss) = - ((Args.parens (Scan.repeat Parse.short_ident) - >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s])) - |> Scan.option |> Scan.lift) + (Scan.lift (Scan.optional + (Args.parens (Parse.short_ident + -- Scan.option (Parse.$$$ "," |-- Parse.short_ident)) + >> (fn (s, s') => + (NONE, NONE) + |> consider_arg s + |> (case s' of SOME s' => consider_arg s' | _ => I))) + (NONE, NONE))) -- Attrib.thms >> (METHOD oo method type_syss) |> Method.setup binding diff -r 25388cf06437 -r 973bb7846505 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:20:58 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Nov 16 09:42:27 2011 +0100 @@ -24,7 +24,6 @@ val metis_generated_var_prefix : string val trace : bool Config.T val verbose : bool Config.T - val lambda_trans : string Config.T val trace_msg : Proof.context -> (unit -> string) -> unit val verbose_warning : Proof.context -> string -> unit val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list @@ -52,8 +51,6 @@ val trace = Attrib.setup_config_bool @{binding metis_trace} (K false) val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true) -val lambda_trans = - Attrib.setup_config_string @{binding metis_lambda_trans} (K combinatorsN) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () fun verbose_warning ctxt msg = @@ -202,7 +199,7 @@ | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula" (* Function to generate metis clauses, including comb and type clauses *) -fun prepare_metis_problem ctxt type_enc lambda_trans conj_clauses fact_clauses = +fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses = let val (conj_clauses, fact_clauses) = if polymorphism_of_type_enc type_enc = Polymorphic then @@ -232,10 +229,9 @@ tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt o snd) props)) *) - val lambda_trans = - if lambda_trans = combinatorsN then no_lamsN else lambda_trans + val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans val (atp_problem, _, _, _, _, _, lifted, sym_tab) = - prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans + prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans false false [] @{prop False} props (* val _ = tracing ("ATP PROBLEM: " ^ diff -r 25388cf06437 -r 973bb7846505 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Nov 15 22:20:58 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 16 09:42:27 2011 +0100 @@ -87,6 +87,7 @@ ("blocking", "false"), ("type_enc", "smart"), ("sound", "false"), + ("lam_trans", "smart"), ("relevance_thresholds", "0.45 0.85"), ("max_relevant", "smart"), ("max_mono_iters", "3"), @@ -108,9 +109,9 @@ ("no_slicing", "slicing")] val params_for_minimize = - ["debug", "verbose", "overlord", "type_enc", "sound", "max_mono_iters", - "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout", - "preplay_timeout"] + ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans", + "max_mono_iters", "max_new_mono_instances", "isar_proof", + "isar_shrink_factor", "timeout", "preplay_timeout"] val property_dependent_params = ["provers", "timeout"] @@ -137,8 +138,10 @@ | _ => value) | NONE => (name, value) -(* "provers =" and "type_enc =" can be left out. The latter is a secret - feature. *) +val any_type_enc = type_enc_from_string Sound "erased" + +(* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two, + this is a secret feature. *) fun normalize_raw_param ctxt = unalias_raw_param #> (fn (name, value) => @@ -148,6 +151,9 @@ ("provers", [name]) else if can (type_enc_from_string Sound) name andalso null value then ("type_enc", [name]) + else if can (trans_lams_from_string ctxt any_type_enc) name andalso + null value then + ("lam_trans", [name]) else error ("Unknown parameter: " ^ quote name ^ ".")) @@ -275,6 +281,7 @@ "smart" => NONE | s => (type_enc_from_string Sound s; SOME s) val sound = mode = Auto_Try orelse lookup_bool "sound" + val lam_trans = lookup_string "lam_trans" val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_option lookup_int "max_relevant" val max_mono_iters = lookup_int "max_mono_iters" @@ -290,10 +297,10 @@ val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, - provers = provers, relevance_thresholds = relevance_thresholds, + provers = provers, type_enc = type_enc, sound = sound, + lam_trans = lam_trans, relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, max_mono_iters = max_mono_iters, - max_new_mono_instances = max_new_mono_instances, type_enc = type_enc, - sound = sound, isar_proof = isar_proof, + max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end diff -r 25388cf06437 -r 973bb7846505 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Nov 15 22:20:58 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 09:42:27 2011 +0100 @@ -47,7 +47,7 @@ fun print silent f = if silent then () else Output.urgent_message (f ()) fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, - max_new_mono_instances, type_enc, isar_proof, + max_new_mono_instances, type_enc, lam_trans, isar_proof, isar_shrink_factor, preplay_timeout, ...} : params) silent (prover : prover) timeout i n state facts = let @@ -62,8 +62,8 @@ val params = {debug = debug, verbose = verbose, overlord = overlord, blocking = true, provers = provers, type_enc = type_enc, sound = true, - relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts), - max_mono_iters = max_mono_iters, + lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01), + max_relevant = SOME (length facts), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slicing = false, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} diff -r 25388cf06437 -r 973bb7846505 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 15 22:20:58 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 09:42:27 2011 +0100 @@ -26,6 +26,7 @@ provers: string list, type_enc: string option, sound: bool, + lam_trans: string, relevance_thresholds: real * real, max_relevant: int option, max_mono_iters: int, @@ -62,7 +63,6 @@ val dest_dir : string Config.T val problem_prefix : string Config.T - val atp_lambda_trans : string Config.T val atp_full_names : bool Config.T val smt_triggers : bool Config.T val smt_weights : bool Config.T @@ -297,6 +297,7 @@ provers: string list, type_enc: string option, sound: bool, + lam_trans: string, relevance_thresholds: real * real, max_relevant: int option, max_mono_iters: int, @@ -339,8 +340,6 @@ val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob") -val atp_lambda_trans = - Attrib.setup_config_string @{binding sledgehammer_atp_lambda_trans} (K smartN) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) @@ -412,11 +411,11 @@ in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end fun tac_for_reconstructor Metis = - Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc] + Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc] combinatorsN | tac_for_reconstructor Metis_Full_Types = - Metis_Tactic.metis_tac Metis_Tactic.full_type_syss + Metis_Tactic.metis_tac Metis_Tactic.full_type_syss combinatorsN | tac_for_reconstructor Metis_No_Types = - Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] + Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] combinatorsN | tac_for_reconstructor SMT = SMT_Solver.smt_tac fun timed_reconstructor reconstructor debug timeout ths = @@ -561,7 +560,7 @@ fun run_atp mode name ({exec, required_execs, arguments, proof_delims, known_failures, conj_sym_kind, prem_kind, best_slices, ...} : atp_config) - ({debug, verbose, overlord, type_enc, sound, max_relevant, + ({debug, verbose, overlord, type_enc, sound, lam_trans, max_relevant, max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params) minimize_command @@ -670,12 +669,12 @@ |> Output.urgent_message else () + val readable_names = not (Config.get ctxt atp_full_names) val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, _, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind - type_enc false (Config.get ctxt atp_lambda_trans) - (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t - facts + type_enc false lam_trans readable_names true hyp_ts + concl_t facts fun weights () = atp_problem_weights atp_problem val full_proof = debug orelse isar_proof val core = diff -r 25388cf06437 -r 973bb7846505 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Tue Nov 15 22:20:58 2011 +0100 +++ b/src/HOL/ex/sledgehammer_tactics.ML Wed Nov 16 09:42:27 2011 +0100 @@ -71,7 +71,8 @@ fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th = case run_atp override_params relevance_override i i ctxt th of SOME facts => - Metis_Tactic.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th + Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt + (maps (thms_of_name ctxt) facts) i th | NONE => Seq.empty fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =