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