--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 08 22:17:53 2010 +0100
@@ -457,7 +457,7 @@
("provers", prover_name),
("timeout", Int.toString timeout)]
val minimize =
- Sledgehammer_Minimize.minimize_facts params 1
+ Sledgehammer_Minimize.minimize_facts params true 1
(Sledgehammer_Util.subgoal_count st)
val _ = log separator
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 08 22:17:53 2010 +0100
@@ -15,10 +15,10 @@
val conjecture_prefix : string
val translate_atp_fact :
Proof.context -> (string * 'a) * thm
- -> term * ((string * 'a) * translated_formula) option
+ -> translated_formula option * ((string * 'a) * thm)
val prepare_atp_problem :
Proof.context -> bool -> bool -> bool -> bool -> term list -> term
- -> (term * ((string * 'a) * translated_formula) option) list
+ -> (translated_formula option * ((string * 'a) * thm)) list
-> string problem * string Symtab.table * int * (string * 'a) list vector
end;
@@ -194,10 +194,10 @@
ctypes_sorts = ctypes_sorts}
end
-fun make_fact ctxt presimp ((name, loc), th) =
+fun make_fact ctxt presimp ((name, _), th) =
case make_formula ctxt presimp name Axiom (prop_of th) of
{combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
- | formula => SOME ((name, loc), formula)
+ | formula => SOME formula
fun make_conjecture ctxt ts =
let val last = length ts - 1 in
map2 (fn j => make_formula ctxt true (Int.toString j)
@@ -244,16 +244,20 @@
|> maps (fn (ss, ths) =>
if exists is_needed ss then map baptize ths else [])) @
(if is_FO then [] else map baptize mandatory_helpers)
- |> map_filter (Option.map snd o make_fact ctxt false)
+ |> map_filter (make_fact ctxt false)
end
-fun translate_atp_fact ctxt (ax as (_, th)) =
- (prop_of th, make_fact ctxt true ax)
+fun translate_atp_fact ctxt = `(make_fact ctxt true)
-fun translate_formulas ctxt full_types hyp_ts concl_t facts =
+fun translate_formulas ctxt full_types hyp_ts concl_t rich_facts =
let
val thy = ProofContext.theory_of ctxt
- val (fact_ts, translated_facts) = ListPair.unzip facts
+ val fact_ts = map (prop_of o snd o snd) rich_facts
+ val (facts, fact_names) =
+ rich_facts
+ |> map_filter (fn (NONE, _) => NONE
+ | (SOME fact, (name, _)) => SOME (fact, name))
+ |> ListPair.unzip
(* Remove existing facts from the conjecture, as this can dramatically
boost an ATP's performance (for some reason). *)
val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
@@ -264,7 +268,6 @@
val tycons = type_consts_of_terms thy (goal_t :: fact_ts)
(* TFrees in the conjecture; TVars in the facts *)
val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
- val (fact_names, facts) = ListPair.unzip (map_filter I translated_facts)
val helper_facts = get_helper_facts ctxt is_FO full_types conjectures facts
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 22:17:53 2010 +0100
@@ -10,8 +10,12 @@
type locality = Sledgehammer_Filter.locality
type params = Sledgehammer_Provers.params
+ val filter_used_facts :
+ (string * locality) list -> ((string * locality) * thm list) list
+ -> ((string * locality) * thm list) list
val minimize_facts :
- params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
+ params -> bool -> int -> int -> Proof.state
+ -> ((string * locality) * thm list) list
-> ((string * locality) * thm list) list option * string
val run_minimize :
params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
@@ -42,12 +46,13 @@
"")
end
+fun print silent f = if silent then () else Output.urgent_message (f ())
+
fun test_facts ({debug, overlord, provers, full_types, isar_proof,
- isar_shrink_factor, ...} : params) (prover : prover)
+ isar_shrink_factor, ...} : params) silent (prover : prover)
explicit_apply timeout i n state facts =
let
- val _ =
- Output.urgent_message ("Testing " ^ n_facts (map fst facts) ^ "...")
+ val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...")
val params =
{blocking = true, debug = debug, verbose = false, overlord = overlord,
provers = provers, full_types = full_types,
@@ -62,12 +67,12 @@
facts = facts}
val result as {outcome, used_facts, ...} = prover params (K "") problem
in
- Output.urgent_message
- (case outcome of
- SOME failure => string_for_failure failure
- | NONE =>
- if length used_facts = length facts then "Found proof."
- else "Found proof with " ^ n_facts used_facts ^ ".");
+ print silent
+ (fn () => case outcome of
+ SOME failure => string_for_failure failure
+ | NONE =>
+ if length used_facts = length facts then "Found proof."
+ else "Found proof with " ^ n_facts used_facts ^ ".");
result
end
@@ -121,15 +126,15 @@
part of the timeout. *)
val fudge_msecs = 1000
-fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."
- | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n
- state facts =
+fun minimize_facts {provers = [], ...} _ _ _ _ _ = error "No prover is set."
+ | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) silent
+ i n state facts =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val prover = get_prover ctxt false prover_name
val msecs = Time.toMilliseconds timeout
- val _ = Output.urgent_message ("Sledgehammer minimize: " ^
+ val _ = print silent (fn () => "Sledgehammer minimize: " ^
quote prover_name ^ ".")
val {goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
@@ -137,7 +142,7 @@
not (forall (Meson.is_fol_term thy)
(concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
fun do_test timeout =
- test_facts params prover explicit_apply timeout i n state
+ test_facts params silent prover explicit_apply timeout i n state
val timer = Timer.startRealTimer ()
in
(case do_test timeout facts of
@@ -154,7 +159,7 @@
else
sublinear_minimize (do_test new_timeout) facts ([], result)
val n = length min_thms
- val _ = Output.urgent_message (cat_lines
+ val _ = print silent (fn () => cat_lines
["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of
0 => ""
@@ -180,13 +185,14 @@
val reserved = reserved_isar_keyword_table ()
val chained_ths = #facts (Proof.goal state)
val facts =
- maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) refs
+ refs
+ |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
in
case subgoal_count state of
0 => Output.urgent_message "No subgoal!"
| n =>
(kill_provers ();
- Output.urgent_message (#2 (minimize_facts params i n state facts)))
+ Output.urgent_message (#2 (minimize_facts params false i n state facts)))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 08 22:17:53 2010 +0100
@@ -32,7 +32,7 @@
datatype prover_fact =
Untranslated_Fact of (string * locality) * thm |
ATP_Translated_Fact of
- term * ((string * locality) * translated_formula) option
+ translated_formula option * ((string * locality) * thm)
type prover_problem =
{state: Proof.state,
@@ -62,6 +62,7 @@
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
+ val untranslated_fact : prover_fact -> (string * locality) * thm
val available_provers : Proof.context -> unit
val kill_provers : unit -> unit
val running_provers : unit -> unit
@@ -213,8 +214,7 @@
datatype prover_fact =
Untranslated_Fact of (string * locality) * thm |
- ATP_Translated_Fact of
- term * ((string * locality) * translated_formula) option
+ ATP_Translated_Fact of translated_formula option * ((string * locality) * thm)
type prover_problem =
{state: Proof.state,
@@ -254,11 +254,10 @@
(* generic TPTP-based ATPs *)
-fun dest_Untranslated_Fact (Untranslated_Fact p) = p
- | dest_Untranslated_Fact (ATP_Translated_Fact _) =
- raise Fail "dest_Untranslated_Fact"
+fun untranslated_fact (Untranslated_Fact p) = p
+ | untranslated_fact (ATP_Translated_Fact (_, p)) = p
fun atp_translated_fact ctxt (Untranslated_Fact p) = translate_atp_fact ctxt p
- | atp_translated_fact _ (ATP_Translated_Fact p) = p
+ | atp_translated_fact _ (ATP_Translated_Fact q) = q
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
| int_opt_add _ _ = NONE
@@ -276,8 +275,7 @@
let
val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
- val facts =
- facts |> map (atp_translated_fact ctxt)
+ val facts = facts |> map (atp_translated_fact ctxt)
val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
else Config.get ctxt dest_dir
val problem_prefix = Config.get ctxt problem_prefix
@@ -530,9 +528,7 @@
#> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
val state = state |> Proof.map_context repair_context
val thy = Proof.theory_of state
- val get_fact =
- Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated_Fact
- val facts = facts |> map_filter get_fact
+ val facts = facts |> map (apsnd (Thm.transfer thy) o untranslated_fact)
val {outcome, used_facts, run_time_in_msecs} =
smt_filter_loop params remote state subgoal facts
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 08 22:17:53 2010 +0100
@@ -24,6 +24,7 @@
open Sledgehammer_Filter
open Sledgehammer_ATP_Translate
open Sledgehammer_Provers
+open Sledgehammer_Minimize
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
n goal =
@@ -38,6 +39,8 @@
else
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+val implicit_minimization_threshold = 50
+
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
auto minimize_command only
{state, goal, subgoal, subgoal_count, facts} name =
@@ -58,8 +61,18 @@
let
fun really_go () =
prover params (minimize_command name) problem
- |> (fn {outcome, message, ...} =>
- (if is_some outcome then "none" else "some", message))
+ |> (fn {outcome, used_facts, message, ...} =>
+ if is_some outcome then
+ ("none", message)
+ else
+ ("some",
+ if length used_facts >= implicit_minimization_threshold then
+ minimize_facts params true subgoal subgoal_count state
+ (filter_used_facts used_facts
+ (map (apsnd single o untranslated_fact) facts))
+ |> snd
+ else
+ message))
val (outcome_code, message) =
if debug then
really_go ()
@@ -84,8 +97,8 @@
if auto then
let val (success, message) = TimeLimit.timeLimit timeout go () in
(success, state |> success ? Proof.goal_message (fn () =>
- Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
- (Pretty.str message)]))
+ Pretty.chunks [Pretty.str "",
+ Pretty.mark Markup.hilite (Pretty.str message)]))
end
else if blocking then
let val (success, message) = TimeLimit.timeLimit timeout go () in
@@ -101,9 +114,6 @@
(* FUDGE *)
val auto_max_relevant_divisor = 2
-fun fact_name (Untranslated_Fact ((name, _), _)) = SOME name
- | fact_name (ATP_Translated_Fact (_, p)) = Option.map (fst o fst) p
-
fun run_sledgehammer (params as {blocking, debug, provers, full_types,
relevance_thresholds, max_relevant, ...})
auto i (relevance_override as {only, ...}) minimize_command
@@ -156,7 +166,7 @@
else
"Including (up to) " ^ string_of_int (length facts) ^
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^
- (facts |> map_filter fact_name
+ (facts |> map (fst o fst o untranslated_fact)
|> space_implode " ") ^ "."))
else
();