--- 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