1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:04 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:04 2012 +0200
1.3 @@ -17,13 +17,15 @@
1.4 val auto_minimize_min_facts : int Config.T
1.5 val auto_minimize_max_time : real Config.T
1.6 val minimize_facts :
1.7 - string -> params -> bool -> int -> int -> Proof.state
1.8 + (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state
1.9 -> ((string * stature) * thm list) list
1.10 -> ((string * stature) * thm list) list option
1.11 * ((unit -> play) * (play -> string) * string)
1.12 - val get_minimizing_prover : Proof.context -> mode -> string -> prover
1.13 + val get_minimizing_prover :
1.14 + Proof.context -> mode -> (thm list -> unit) -> string -> prover
1.15 val run_minimize :
1.16 - params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
1.17 + params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
1.18 + -> Proof.state -> unit
1.19 end;
1.20
1.21 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
1.22 @@ -68,7 +70,7 @@
1.23 {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
1.24 provers = provers, type_enc = type_enc, strict = strict,
1.25 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
1.26 - fact_filter = NONE, max_facts = SOME (length facts),
1.27 + learn = false, fact_filter = NONE, max_facts = SOME (length facts),
1.28 fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
1.29 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
1.30 isar_shrink_factor = isar_shrink_factor, slice = false,
1.31 @@ -181,8 +183,8 @@
1.32 | p => p
1.33 end
1.34
1.35 -fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
1.36 - facts =
1.37 +fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
1.38 + i n state facts =
1.39 let
1.40 val ctxt = Proof.context_of state
1.41 val prover =
1.42 @@ -202,13 +204,16 @@
1.43 linear_minimize
1.44 val (min_facts, {preplay, message, message_tail, ...}) =
1.45 min test (new_timeout timeout run_time) result facts
1.46 - val _ = print silent (fn () => cat_lines
1.47 - ["Minimized to " ^ n_facts (map fst min_facts)] ^
1.48 - (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
1.49 - |> length of
1.50 - 0 => ""
1.51 - | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
1.52 - in (SOME min_facts, (preplay, message, message_tail)) end
1.53 + in
1.54 + print silent (fn () => cat_lines
1.55 + ["Minimized to " ^ n_facts (map fst min_facts)] ^
1.56 + (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
1.57 + |> length of
1.58 + 0 => ""
1.59 + | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
1.60 + (if learn then do_learn (maps snd min_facts) else ());
1.61 + (SOME min_facts, (preplay, message, message_tail))
1.62 + end
1.63 | {outcome = SOME TimedOut, preplay, ...} =>
1.64 (NONE,
1.65 (preplay,
1.66 @@ -225,9 +230,10 @@
1.67
1.68 fun adjust_reconstructor_params override_params
1.69 ({debug, verbose, overlord, blocking, provers, type_enc, strict,
1.70 - lam_trans, uncurried_aliases, fact_filter, max_facts, fact_thresholds,
1.71 - max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
1.72 - slice, minimize, timeout, preplay_timeout, expect} : params) =
1.73 + lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
1.74 + fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proof,
1.75 + isar_shrink_factor, slice, minimize, timeout, preplay_timeout, expect}
1.76 + : params) =
1.77 let
1.78 fun lookup_override name default_value =
1.79 case AList.lookup (op =) override_params name of
1.80 @@ -241,7 +247,7 @@
1.81 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
1.82 provers = provers, type_enc = type_enc, strict = strict,
1.83 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
1.84 - fact_filter = fact_filter, max_facts = max_facts,
1.85 + learn = learn, fact_filter = fact_filter, max_facts = max_facts,
1.86 fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
1.87 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
1.88 isar_shrink_factor = isar_shrink_factor, slice = slice,
1.89 @@ -249,7 +255,7 @@
1.90 expect = expect}
1.91 end
1.92
1.93 -fun minimize ctxt mode name
1.94 +fun minimize ctxt mode do_learn name
1.95 (params as {debug, verbose, isar_proof, minimize, ...})
1.96 ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
1.97 (result as {outcome, used_facts, run_time, preplay, message,
1.98 @@ -293,7 +299,7 @@
1.99 val minimize = minimize |> the_default perhaps_minimize
1.100 val (used_facts, (preplay, message, _)) =
1.101 if minimize then
1.102 - minimize_facts minimize_name params (not verbose) subgoal
1.103 + minimize_facts do_learn minimize_name params (not verbose) subgoal
1.104 subgoal_count state
1.105 (filter_used_facts used_facts
1.106 (map (apsnd single o untranslated_fact) facts))
1.107 @@ -319,11 +325,12 @@
1.108 | NONE => result
1.109 end
1.110
1.111 -fun get_minimizing_prover ctxt mode name params minimize_command problem =
1.112 +fun get_minimizing_prover ctxt mode do_learn name params minimize_command
1.113 + problem =
1.114 get_prover ctxt mode name params minimize_command problem
1.115 - |> minimize ctxt mode name params problem
1.116 + |> minimize ctxt mode do_learn name params problem
1.117
1.118 -fun run_minimize (params as {provers, ...}) i refs state =
1.119 +fun run_minimize (params as {provers, ...}) do_learn i refs state =
1.120 let
1.121 val ctxt = Proof.context_of state
1.122 val reserved = reserved_isar_keyword_table ()
1.123 @@ -339,7 +346,7 @@
1.124 [] => error "No prover is set."
1.125 | prover :: _ =>
1.126 (kill_provers ();
1.127 - minimize_facts prover params false i n state facts
1.128 + minimize_facts do_learn prover params false i n state facts
1.129 |> (fn (_, (preplay, message, message_tail)) =>
1.130 message (preplay ()) ^ message_tail
1.131 |> Output.urgent_message))