killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 08:47:43 2011 +0200
@@ -131,8 +131,7 @@
val type_constrs_of_terms : theory -> term list -> string list
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_sys
- -> bool option -> bool -> bool -> term list -> term
- -> ((string * locality) * term) list
+ -> bool -> bool -> term list -> term -> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
* (string * locality) list vector * int list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
@@ -1833,9 +1832,10 @@
val conjsN = "Conjectures"
val free_typesN = "Type variables"
+val explicit_apply = NONE (* for experimental purposes *)
+
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
- explicit_apply readable_names preproc hyp_ts concl_t
- facts =
+ readable_names preproc hyp_ts concl_t facts =
let
val (format, type_sys) = choose_format [format] type_sys
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 08:47:43 2011 +0200
@@ -706,7 +706,7 @@
val ax_counts =
Int_Tysubst_Table.empty
|> fold (fn (ax_no, (_, (tysubst, _))) =>
- Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
+ Int_Tysubst_Table.map_default ((ax_no, [](*###*)), 0)
(Integer.add 1)) substs
|> Int_Tysubst_Table.dest
val needed_axiom_props =
--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 08:47:43 2011 +0200
@@ -167,7 +167,6 @@
fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
let
val type_sys = type_sys_from_string type_sys
- val explicit_apply = NONE
val clauses =
conj_clauses @ fact_clauses
|> (if polymorphism_of_type_sys type_sys = Polymorphic then
@@ -188,8 +187,8 @@
val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
- false false props @{prop False} []
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props
+ @{prop False} []
(*
val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 08 08:47:43 2011 +0200
@@ -96,7 +96,6 @@
("max_relevant", "smart"),
("max_mono_iters", "3"),
("max_new_mono_instances", "400"),
- ("explicit_apply", "smart"),
("isar_proof", "false"),
("isar_shrink_factor", "1"),
("slicing", "true"),
@@ -112,14 +111,13 @@
("no_overlord", "overlord"),
("non_blocking", "blocking"),
("partial_types", "full_types"),
- ("implicit_apply", "explicit_apply"),
("no_isar_proof", "isar_proof"),
("no_slicing", "slicing")]
val params_for_minimize =
["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
- "max_new_mono_instances", "explicit_apply", "isar_proof",
- "isar_shrink_factor", "timeout", "preplay_timeout"]
+ "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
+ "preplay_timeout"]
val property_dependent_params = ["provers", "full_types", "timeout"]
@@ -284,7 +282,6 @@
val max_relevant = lookup_option lookup_int "max_relevant"
val max_mono_iters = lookup_int "max_mono_iters"
val max_new_mono_instances = lookup_int "max_new_mono_instances"
- val explicit_apply = lookup_option lookup_bool "explicit_apply"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
@@ -299,9 +296,9 @@
provers = provers, relevance_thresholds = relevance_thresholds,
max_relevant = max_relevant, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
- explicit_apply = explicit_apply, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, slicing = slicing,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+ slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout,
+ expect = expect}
end
fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 08 08:47:43 2011 +0200
@@ -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_sys, explicit_apply, isar_proof,
+ max_new_mono_instances, type_sys, isar_proof,
isar_shrink_factor, preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state facts =
let
@@ -59,7 +59,7 @@
val {goal, ...} = Proof.goal state
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
- provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
+ provers = provers, type_sys = type_sys,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
@@ -73,16 +73,18 @@
val result as {outcome, used_facts, run_time_in_msecs, ...} =
prover params (K (K "")) problem
in
- print silent (fn () =>
- case outcome of
- SOME failure => string_for_failure failure
- | NONE => "Found proof" ^
- (if length used_facts = length facts then ""
- else " with " ^ n_facts used_facts) ^
- (case run_time_in_msecs of
- SOME ms =>
- " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
- | NONE => "") ^ ".");
+ print silent
+ (fn () =>
+ case outcome of
+ SOME failure => string_for_failure failure
+ | NONE =>
+ "Found proof" ^
+ (if length used_facts = length facts then ""
+ else " with " ^ n_facts used_facts) ^
+ (case run_time_in_msecs of
+ SOME ms =>
+ " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
+ | NONE => "") ^ ".");
result
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jun 08 08:47:43 2011 +0200
@@ -33,7 +33,6 @@
max_relevant: int option,
max_mono_iters: int,
max_new_mono_instances: int,
- explicit_apply: bool option,
isar_proof: bool,
isar_shrink_factor: int,
slicing: bool,
@@ -301,7 +300,6 @@
max_relevant: int option,
max_mono_iters: int,
max_new_mono_instances: int,
- explicit_apply: bool option,
isar_proof: bool,
isar_shrink_factor: int,
slicing: bool,
@@ -549,8 +547,8 @@
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
- max_new_mono_instances, explicit_apply, isar_proof,
- isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
+ max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
+ timeout, preplay_timeout, ...} : params)
minimize_command
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
@@ -655,9 +653,8 @@
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_sys explicit_apply
- (Config.get ctxt atp_readable_names) true hyp_ts concl_t
- facts
+ type_sys (Config.get ctxt atp_readable_names) true hyp_ts
+ concl_t facts
fun weights () = atp_problem_weights atp_problem
val core =
File.shell_path command ^ " " ^
--- a/src/HOL/ex/atp_export.ML Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Wed Jun 08 08:47:43 2011 +0200
@@ -102,11 +102,10 @@
val facts =
facts0 |> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc), prop_of th))
- val explicit_apply = NONE
val (atp_problem, _, _, _, _, _, _) =
ATP_Translate.prepare_atp_problem ctxt format
- ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
- [] @{prop False} facts
+ ATP_Problem.Axiom ATP_Problem.Axiom type_sys false true []
+ @{prop False} facts
val infers =
facts0 |> map (fn (_, th) =>
(fact_name_of (Thm.get_name_hint th),