--- 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
--- 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
--- 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
--- 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: " ^
--- 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
--- 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 = ""}
--- 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 =
--- 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 =