--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 15:19:07 2014 +0100
@@ -12,7 +12,7 @@
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
type fact = Sledgehammer_Fact.fact
- type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type proof_method = Sledgehammer_Reconstructor.proof_method
type play_outcome = Sledgehammer_Reconstructor.play_outcome
type minimize_command = Sledgehammer_Reconstructor.minimize_command
@@ -57,8 +57,8 @@
used_facts : (string * stature) list,
used_from : fact list,
run_time : Time.time,
- preplay : (reconstructor * play_outcome) Lazy.lazy,
- message : reconstructor * play_outcome -> string,
+ preplay : (proof_method * play_outcome) Lazy.lazy,
+ message : proof_method * play_outcome -> string,
message_tail : string}
type prover =
@@ -66,23 +66,22 @@
-> prover_problem -> prover_result
val SledgehammerN : string
- val plain_metis : reconstructor
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
- val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
- val is_reconstructor : string -> bool
+ val extract_proof_method : params -> proof_method -> string * (string * string list) list
+ val is_proof_method : string -> bool
val is_atp : theory -> string -> bool
- val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
+ val bunch_of_proof_methods : bool -> string -> proof_method list
val is_fact_chained : (('a * stature) * 'b) -> bool
val filter_used_facts :
bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
- Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome
+ Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
val remotify_atp_if_not_installed : theory -> string -> string option
val isar_supported_prover_of : theory -> string -> string
val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
- string -> reconstructor * play_outcome -> 'a
+ string -> proof_method * play_outcome -> 'a
val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
Proof.context
@@ -110,9 +109,8 @@
"Async_Manager". *)
val SledgehammerN = "Sledgehammer"
-val reconstructor_names = [metisN, smtN]
-val plain_metis = Metis (hd partial_type_encs, combsN)
-val is_reconstructor = member (op =) reconstructor_names
+val proof_method_names = [metisN, smtN]
+val is_proof_method = member (op =) proof_method_names
val is_atp = member (op =) o supported_atps
@@ -167,8 +165,8 @@
used_facts : (string * stature) list,
used_from : fact list,
run_time : Time.time,
- preplay : (reconstructor * play_outcome) Lazy.lazy,
- message : reconstructor * play_outcome -> string,
+ preplay : (proof_method * play_outcome) Lazy.lazy,
+ message : proof_method * play_outcome -> string,
message_tail : string}
type prover =
@@ -183,29 +181,30 @@
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
| _ => "Try this")
-fun bunch_of_reconstructors needs_full_types lam_trans =
+fun bunch_of_proof_methods needs_full_types desperate_lam_trans =
if needs_full_types then
- [Metis (full_type_enc, lam_trans false),
- Metis (really_full_type_enc, lam_trans false),
- Metis (full_type_enc, lam_trans true),
- Metis (really_full_type_enc, lam_trans true),
- SMT]
+ [Metis_Method (SOME full_type_enc, NONE),
+ Metis_Method (SOME really_full_type_enc, NONE),
+ Metis_Method (SOME full_type_enc, SOME desperate_lam_trans),
+ Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
+ SMT_Method]
else
- [Metis (partial_type_enc, lam_trans false),
- Metis (full_type_enc, lam_trans false),
- Metis (no_typesN, lam_trans true),
- Metis (really_full_type_enc, lam_trans true),
- SMT]
+ [Metis_Method (NONE, NONE),
+ Metis_Method (SOME full_type_enc, NONE),
+ Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
+ Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
+ SMT_Method]
-fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
+fun extract_proof_method ({type_enc, lam_trans, ...} : params)
+ (Metis_Method (type_enc', lam_trans')) =
let
val override_params =
- (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
- else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
- (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
- else [("lam_trans", [lam_trans'])])
+ (if is_none type_enc' andalso is_none type_enc then []
+ else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
+ (if is_none lam_trans' andalso is_none lam_trans then []
+ else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
in (metisN, override_params) end
- | extract_reconstructor _ SMT = (smtN, [])
+ | extract_proof_method _ SMT_Method = (smtN, [])
(* based on "Mirabelle.can_apply" and generalized *)
fun timed_apply timeout tac state i =
@@ -216,49 +215,46 @@
TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
end
-fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
- | tac_of_reconstructor SMT = SMT_Solver.smt_tac
-
-fun timed_reconstructor reconstr debug timeout ths =
- timed_apply timeout (silence_reconstructors debug
- #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
+(* FIXME *)
+fun timed_proof_method meth debug timeout ths =
+ timed_apply timeout (silence_proof_methods debug
+ #> (fn ctxt => tac_of_proof_method ctxt ([], ths) meth))
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
fun filter_used_facts keep_chained used =
filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
-fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
+fun play_one_line_proof mode debug verbose timeout pairs state i preferred meths =
let
- fun get_preferred reconstrs =
- if member (op =) reconstrs preferred then preferred
- else List.last reconstrs
+ fun get_preferred meths =
+ if member (op =) meths preferred then preferred else List.last meths
in
if timeout = Time.zeroTime then
- (get_preferred reconstrs, Not_Played)
+ (get_preferred meths, Not_Played)
else
let
val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
val ths = pairs |> sort_wrt (fst o fst) |> map snd
- fun play [] [] = (get_preferred reconstrs, Play_Failed)
+ fun play [] [] = (get_preferred meths, Play_Failed)
| play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
- | play timed_out (reconstr :: reconstrs) =
+ | play timed_out (meth :: meths) =
let
val _ =
if verbose then
- Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
+ Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
"\" for " ^ string_of_time timeout ^ "...")
else
()
val timer = Timer.startRealTimer ()
in
- case timed_reconstructor reconstr debug timeout ths state i of
- SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
- | _ => play timed_out reconstrs
+ case timed_proof_method meth debug timeout ths state i of
+ SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
+ | _ => play timed_out meths
end
- handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
+ handle TimeLimit.TimeOut => play (meth :: timed_out) meths
in
- play [] reconstrs
+ play [] meths
end
end
@@ -275,9 +271,8 @@
val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
val (min_name, override_params) =
(case preplay of
- (reconstr, Played _) =>
- if isar_proofs = SOME true then (maybe_isar_name, [])
- else extract_reconstructor params reconstr
+ (meth, Played _) =>
+ if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
| _ => (maybe_isar_name, []))
in minimize_command override_params min_name end
@@ -293,7 +288,7 @@
let
val thy = Proof_Context.theory_of ctxt
val (remote_provers, local_provers) =
- reconstructor_names @
+ proof_method_names @
sort_strings (supported_atps thy) @
sort_strings (SMT_Solver.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)