--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 16 13:22:36 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 16 16:35:19 2011 +0100
@@ -432,7 +432,7 @@
subgoal_count = Sledgehammer_Util.subgoal_count st,
facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
smt_filter = NONE}
- in prover params (K (K "")) problem end)) ()
+ in prover params (K (K (K ""))) problem end)) ()
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
val time_prover = run_time |> Time.toMilliseconds
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Nov 16 13:22:36 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Nov 16 16:35:19 2011 +0100
@@ -30,6 +30,7 @@
* (string * locality) list vector * int Symtab.table * string proof * thm
val metisN : string
+ val smtN : string
val full_typesN : string
val partial_typesN : string
val no_typesN : string
@@ -198,9 +199,10 @@
| _ => false)
-(** Soft-core proof reconstruction: Metis one-liner **)
+(** Soft-core proof reconstruction: one-liners **)
val metisN = "metis"
+val smtN = "smt"
val full_typesN = "full_types"
val partial_typesN = "partial_types"
@@ -233,12 +235,12 @@
| _ => type_enc
val opts = [] |> type_enc <> Metis_Tactic.partial_typesN ? cons type_enc
|> lam_trans <> metis_default_lam_trans ? cons lam_trans
- in "metis" ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
+ in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
(* unfortunate leaking abstraction *)
fun name_of_reconstructor (Metis (type_enc, lam_trans)) =
metis_call type_enc lam_trans
- | name_of_reconstructor SMT = "smt"
+ | name_of_reconstructor SMT = smtN
fun string_for_label (s, num) = s ^ string_of_int num
@@ -257,9 +259,9 @@
fun using_labels [] = ""
| using_labels ls =
"using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun reconstructor_command reconstructor i n (ls, ss) =
+fun reconstructor_command reconstr i n (ls, ss) =
using_labels ls ^ apply_on_subgoal i n ^
- command_call (name_of_reconstructor reconstructor) ss
+ command_call (name_of_reconstructor reconstr) ss
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
@@ -274,20 +276,19 @@
subgoal, subgoal_count) =
let
val (chained, extra) = split_used_facts used_facts
- val (failed, reconstructor, ext_time) =
+ val (failed, reconstr, ext_time) =
case preplay of
- Played (reconstructor, time) =>
- (false, reconstructor, (SOME (false, time)))
- | Trust_Playable (reconstructor, time) =>
- (false, reconstructor,
+ Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
+ | Trust_Playable (reconstr, time) =>
+ (false, reconstr,
case time of
NONE => NONE
| SOME time =>
if time = Time.zeroTime then NONE else SOME (true, time))
- | Failed_to_Play reconstructor => (true, reconstructor, NONE)
+ | Failed_to_Play reconstr => (true, reconstr, NONE)
val try_line =
([], map fst extra)
- |> reconstructor_command reconstructor subgoal subgoal_count
+ |> reconstructor_command reconstr subgoal subgoal_count
|> (if failed then enclose "One-line proof reconstruction failed: " "."
else try_command_line banner ext_time)
in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
@@ -1008,11 +1009,11 @@
else
if member (op =) qs Show then "show" else "have")
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
- val reconstructor =
+ val reconstr =
Metis (if full_types then Metis_Tactic.full_typesN
else Metis_Tactic.partial_typesN, combinatorsN)
fun do_facts (ls, ss) =
- reconstructor_command reconstructor 1 1
+ reconstructor_command reconstr 1 1
(ls |> sort_distinct (prod_ord string_ord int_ord),
ss |> sort_distinct string_ord)
and do_step ind (Fix xs) =
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Nov 16 13:22:36 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Nov 16 16:35:19 2011 +0100
@@ -37,7 +37,6 @@
val combinatorsN : string
val hybrid_lamsN : string
val keep_lamsN : string
- val smartN : string
val schematic_var_prefix : string
val fixed_var_prefix : string
val tvar_prefix : string
@@ -127,7 +126,6 @@
val combinatorsN = "combinators"
val hybrid_lamsN = "hybrid_lams"
val keep_lamsN = "keep_lams"
-val smartN = "smart"
(* TFF1 is still in development, and it is still unclear whether symbols will be
allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
@@ -2344,10 +2342,8 @@
else
SOME false
val lam_trans =
- if lam_trans = smartN then
- if is_type_enc_higher_order type_enc then keep_lamsN else combinatorsN
- else if lam_trans = keep_lamsN andalso
- not (is_type_enc_higher_order type_enc) then
+ if lam_trans = keep_lamsN andalso
+ not (is_type_enc_higher_order type_enc) then
error ("Lambda translation scheme incompatible with first-order \
\encoding.")
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 16 13:22:36 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 16 16:35:19 2011 +0100
@@ -282,7 +282,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 lam_trans = lookup_option 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"
@@ -318,10 +318,13 @@
fun string_for_raw_param (key, values) =
key ^ (case implode_param values of "" => "" | value => " = " ^ value)
-fun minimize_command override_params i prover_name fact_names =
+fun minimize_command override_params i more_override_params prover_name
+ fact_names =
let
val params =
- override_params
+ (override_params
+ |> filter_out (AList.defined (op =) more_override_params o fst)) @
+ more_override_params
|> filter is_raw_param_relevant_for_minimize
|> map string_for_raw_param
|> (if prover_name = default_minimize_prover then I else cons prover_name)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 13:22:36 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 16:35:19 2011 +0100
@@ -71,7 +71,7 @@
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}
val result as {outcome, used_facts, run_time, ...} =
- prover params (K (K "")) problem
+ prover params (K (K (K ""))) problem
in
print silent
(fn () =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 13:22:36 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 16:35:19 2011 +0100
@@ -26,7 +26,7 @@
provers: string list,
type_enc: string option,
sound: bool,
- lam_trans: string,
+ lam_trans: string option,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -59,7 +59,8 @@
message_tail: string}
type prover =
- params -> (string -> minimize_command) -> prover_problem -> prover_result
+ params -> ((string * string list) list -> string -> minimize_command)
+ -> prover_problem -> prover_result
val dest_dir : string Config.T
val problem_prefix : string Config.T
@@ -78,7 +79,8 @@
val das_tool : string
val plain_metis : reconstructor
val select_smt_solver : string -> Proof.context -> Proof.context
- val prover_name_for_reconstructor : reconstructor -> string
+ val extract_reconstructor :
+ reconstructor -> string * (string * string list) list
val is_reconstructor : string -> bool
val is_atp : theory -> string -> bool
val is_smt_prover : Proof.context -> string -> bool
@@ -129,23 +131,26 @@
"Async_Manager". *)
val das_tool = "Sledgehammer"
-val metisN = metisN
-val metis_full_typesN = metisN ^ "_" ^ full_typesN
-val metis_no_typesN = metisN ^ "_" ^ no_typesN
-val smtN = name_of_reconstructor SMT
+fun extract_reconstructor (Metis (type_enc, lam_trans)) =
+ let
+ val override_params =
+ (if type_enc = hd partial_type_encs then []
+ else [("type_enc", [type_enc])]) @
+ (if lam_trans = metis_default_lam_trans then []
+ else [("lam_trans", [lam_trans])])
+ in (metisN, override_params) end
+ | extract_reconstructor SMT = (smtN, [])
+val reconstructor_names = [metisN, smtN]
val plain_metis = Metis (hd partial_type_encs, combinatorsN)
-val reconstructor_infos =
- [(metisN, plain_metis),
- (metis_full_typesN, Metis (hd full_type_encs, combinatorsN)),
- (metis_no_typesN, Metis (no_type_enc, combinatorsN)),
- (smtN, SMT)]
-val prover_name_for_reconstructor = AList.find (op =) reconstructor_infos #> hd
+fun standard_reconstructors lam_trans =
+ [Metis (hd partial_type_encs, lam_trans),
+ Metis (hd full_type_encs, lam_trans),
+ Metis (no_type_enc, lam_trans),
+ SMT]
-val all_reconstructors = map snd reconstructor_infos
-
-val is_reconstructor = AList.defined (op =) reconstructor_infos
+val is_reconstructor = member (op =) reconstructor_names
val is_atp = member (op =) o supported_atps
val select_smt_solver = Context.proof_map o SMT_Config.select_solver
@@ -276,7 +281,7 @@
let
val thy = Proof_Context.theory_of ctxt
val (remote_provers, local_provers) =
- map fst reconstructor_infos @
+ reconstructor_names @
sort_strings (supported_atps thy) @
sort_strings (SMT_Solver.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
@@ -299,7 +304,7 @@
provers: string list,
type_enc: string option,
sound: bool,
- lam_trans: string,
+ lam_trans: string option,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -332,7 +337,8 @@
message_tail: string}
type prover =
- params -> (string -> minimize_command) -> prover_problem -> prover_result
+ params -> ((string * string list) list -> string -> minimize_command)
+ -> prover_problem -> prover_result
(* configuration attributes *)
@@ -416,49 +422,48 @@
Metis_Tactic.metis_tac [type_enc] lam_trans
| tac_for_reconstructor SMT = SMT_Solver.smt_tac
-fun timed_reconstructor reconstructor debug timeout ths =
+fun timed_reconstructor reconstr debug timeout ths =
(Config.put Metis_Tactic.verbose debug
- #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths))
+ #> (fn ctxt => tac_for_reconstructor reconstr ctxt ths))
|> timed_apply timeout
fun filter_used_facts used = filter (member (op =) used o fst)
fun play_one_line_proof mode debug verbose timeout ths state i preferred
- reconstructors =
+ reconstrs =
let
val _ =
if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then
Output.urgent_message "Preplaying proof..."
else
()
- fun get_preferred reconstructors =
- if member (op =) reconstructors preferred then preferred
- else List.last reconstructors
- fun play [] [] = Failed_to_Play (get_preferred reconstructors)
+ fun get_preferred reconstrs =
+ if member (op =) reconstrs preferred then preferred
+ else List.last reconstrs
+ fun play [] [] = Failed_to_Play (get_preferred reconstrs)
| play timed_outs [] =
Trust_Playable (get_preferred timed_outs, SOME timeout)
- | play timed_out (reconstructor :: reconstructors) =
+ | play timed_out (reconstr :: reconstrs) =
let
val _ =
if verbose then
- "Trying \"" ^ name_of_reconstructor reconstructor ^ "\" for " ^
+ "Trying \"" ^ name_of_reconstructor reconstr ^ "\" for " ^
string_from_time timeout ^ "..."
|> Output.urgent_message
else
()
val timer = Timer.startRealTimer ()
in
- case timed_reconstructor reconstructor debug timeout ths state i of
- SOME (SOME _) => Played (reconstructor, Timer.checkRealTimer timer)
- | _ => play timed_out reconstructors
+ case timed_reconstructor reconstr debug timeout ths state i of
+ SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
+ | _ => play timed_out reconstrs
end
- handle TimeLimit.TimeOut =>
- play (reconstructor :: timed_out) reconstructors
+ handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
in
if timeout = Time.zeroTime then
- Trust_Playable (get_preferred reconstructors, NONE)
+ Trust_Playable (get_preferred reconstrs, NONE)
else
- play [] reconstructors
+ play [] reconstrs
end
@@ -532,14 +537,16 @@
val metis_minimize_max_time = seconds 2.0
fun choose_minimize_command minimize_command name preplay =
- (case preplay of
- Played (reconstructor, time) =>
- if Time.<= (time, metis_minimize_max_time) then
- prover_name_for_reconstructor reconstructor
- else
- name
- | _ => name)
- |> minimize_command
+ let
+ val (name, override_params) =
+ case preplay of
+ Played (reconstr, time) =>
+ if Time.<= (time, metis_minimize_max_time) then
+ extract_reconstructor reconstr
+ else
+ (name, [])
+ | _ => (name, [])
+ in minimize_command override_params name end
fun repair_monomorph_context max_iters max_new_instances =
Config.put Monomorph.max_rounds max_iters
@@ -668,6 +675,12 @@
else
()
val readable_names = not (Config.get ctxt atp_full_names)
+ val lam_trans =
+ case lam_trans of
+ SOME s => s
+ | NONE =>
+ if is_type_enc_higher_order type_enc then keep_lamsN
+ else combinatorsN (* FIXME ### improve *)
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, _, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
@@ -725,7 +738,7 @@
| _ => outcome
in
((pool, conjecture_shape, facts_offset, fact_names,
- typed_helpers, sym_tab),
+ typed_helpers, sym_tab, lam_trans),
(output, run_time, atp_proof, outcome))
end
val timer = Timer.startRealTimer ()
@@ -744,8 +757,8 @@
end
| maybe_run_slice _ result = result
in
- ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
- ("", Time.zeroTime, [], SOME InternalError))
+ ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty,
+ no_lamsN), ("", Time.zeroTime, [], SOME InternalError))
|> fold maybe_run_slice actual_slices
end
else
@@ -761,7 +774,7 @@
else
File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
- sym_tab),
+ sym_tab, lam_trans),
(output, run_time, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
val important_message =
@@ -776,6 +789,7 @@
let
val used_facts =
used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof
+ val reconstrs = standard_reconstructors lam_trans
in
(used_facts,
fn () =>
@@ -785,7 +799,7 @@
|> map snd
in
play_one_line_proof mode debug verbose preplay_timeout used_ths
- state subgoal plain_metis all_reconstructors
+ state subgoal (hd reconstrs) reconstrs
end,
fn preplay =>
let
@@ -966,7 +980,8 @@
NONE =>
(fn () =>
play_one_line_proof mode debug verbose preplay_timeout used_ths
- state subgoal SMT all_reconstructors,
+ state subgoal SMT
+ (standard_reconstructors lam_liftingN),
fn preplay =>
let
val one_line_params =
@@ -985,28 +1000,36 @@
preplay = preplay, message = message, message_tail = message_tail}
end
-fun run_reconstructor mode name ({debug, verbose, timeout, ...} : params)
+fun run_reconstructor mode name
+ ({debug, verbose, timeout, type_enc, lam_trans, ...} : params)
minimize_command
({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
- val reconstructor =
- case AList.lookup (op =) reconstructor_infos name of
- SOME r => r
- | NONE => raise Fail ("unknown Metis version: " ^ quote name)
+ val reconstr =
+ if name = metisN then
+ Metis (type_enc |> the_default (hd partial_type_encs),
+ lam_trans |> the_default metis_default_lam_trans)
+ else if name = smtN then
+ SMT
+ else
+ raise Fail ("unknown reconstructor: " ^ quote name)
val (used_facts, used_ths) =
facts |> map untranslated_fact |> ListPair.unzip
in
case play_one_line_proof (if mode = Minimize then Normal else mode) debug
- verbose timeout used_ths state subgoal
- reconstructor [reconstructor] of
+ verbose timeout used_ths state subgoal reconstr
+ [reconstr] of
play as Played (_, time) =>
{outcome = NONE, used_facts = used_facts, run_time = time,
preplay = K play,
message = fn play =>
let
+ val (_, override_params (* FIXME ###: use these *)) =
+ extract_reconstructor reconstr
val one_line_params =
- (play, proof_banner mode name, used_facts,
- minimize_command name, subgoal, subgoal_count)
+ (play, proof_banner mode name, used_facts,
+ minimize_command override_params name, subgoal,
+ subgoal_count)
in one_line_proof_text one_line_params end,
message_tail = ""}
| play =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Nov 16 13:22:36 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Nov 16 16:35:19 2011 +0100
@@ -22,7 +22,8 @@
val auto_minimize_max_time : real Config.T
val get_minimizing_prover : Proof.context -> mode -> string -> prover
val run_sledgehammer :
- params -> mode -> int -> relevance_override -> (string -> minimize_command)
+ params -> mode -> int -> relevance_override
+ -> ((string * string list) list -> string -> minimize_command)
-> Proof.state -> bool * (string * Proof.state)
end;
@@ -71,6 +72,31 @@
Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
(K 5.0)
+fun adjust_reconstructor_params override_params
+ ({debug, verbose, overlord, blocking, provers, type_enc, sound,
+ lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
+ max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
+ timeout, preplay_timeout, expect} : params) =
+ let
+ fun lookup_override name default_value =
+ case AList.lookup (op =) override_params name of
+ SOME [s] => SOME s
+ | _ => default_value
+ (* Only those options that reconstructors are interested in are considered
+ here. *)
+ val type_enc = lookup_override "type_enc" type_enc
+ val lam_trans = lookup_override "lam_trans" lam_trans
+ in
+ {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
+ provers = provers, type_enc = type_enc, sound = sound,
+ lam_trans = lam_trans, max_relevant = max_relevant,
+ relevance_thresholds = relevance_thresholds,
+ 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 = slicing,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ end
+
fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
(result as {outcome, used_facts, run_time, preplay, message,
@@ -80,10 +106,10 @@
else
let
val num_facts = length used_facts
- val ((minimize, minimize_name), preplay) =
+ val ((minimize, (minimize_name, params)), preplay) =
if mode = Normal then
if num_facts >= Config.get ctxt auto_minimize_min_facts then
- ((true, name), preplay)
+ ((true, (name, params)), preplay)
else
let
fun can_min_fast_enough time =
@@ -93,21 +119,24 @@
val prover_fast_enough = can_min_fast_enough run_time
in
if isar_proof then
- ((prover_fast_enough, name), preplay)
+ ((prover_fast_enough, (name, params)), preplay)
else
let val preplay = preplay () in
(case preplay of
- Played (reconstructor, timeout) =>
+ Played (reconstr, timeout) =>
if can_min_fast_enough timeout then
- (true, prover_name_for_reconstructor reconstructor)
+ (true, extract_reconstructor reconstr
+ ||> (fn override_params =>
+ adjust_reconstructor_params
+ override_params params))
else
- (prover_fast_enough, name)
- | _ => (prover_fast_enough, name),
+ (prover_fast_enough, (name, params))
+ | _ => (prover_fast_enough, (name, params)),
K preplay)
end
end
else
- ((false, name), preplay)
+ ((false, (name, params)), preplay)
val (used_facts, (preplay, message, _)) =
if minimize then
minimize_facts minimize_name params (not verbose) subgoal
--- a/src/HOL/ex/sledgehammer_tactics.ML Wed Nov 16 13:22:36 2011 +0100
+++ b/src/HOL/ex/sledgehammer_tactics.ML Wed Nov 16 16:35:19 2011 +0100
@@ -49,7 +49,7 @@
facts = map Sledgehammer_Provers.Untranslated_Fact facts,
smt_filter = NONE}
in
- (case prover params (K (K "")) problem of
+ (case prover params (K (K (K ""))) problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
| _ => NONE)
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)