1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu May 22 03:29:35 2014 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu May 22 03:29:36 2014 +0200
1.3 @@ -51,7 +51,7 @@
1.4 open Sledgehammer_Prover_SMT
1.5 open Sledgehammer_Prover_SMT2
1.6
1.7 -fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
1.8 +fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...})
1.9 minimize_command
1.10 ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
1.11 let
1.12 @@ -61,23 +61,22 @@
1.13 else raise Fail ("unknown proof_method: " ^ quote name)
1.14 val used_facts = facts |> map fst
1.15 in
1.16 - (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout
1.17 - facts state subgoal meth [meth] of
1.18 + (case play_one_line_proof (if mode = Minimize then Normal else mode) verbose timeout facts state
1.19 + subgoal meth [meth] of
1.20 play as (_, Played time) =>
1.21 {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
1.22 preplay = Lazy.value play,
1.23 - message =
1.24 - fn play =>
1.25 - let
1.26 - val ctxt = Proof.context_of state
1.27 - val (_, override_params) = extract_proof_method params meth
1.28 - val one_line_params =
1.29 - (play, proof_banner mode name, used_facts, minimize_command override_params name,
1.30 - subgoal, subgoal_count)
1.31 - val num_chained = length (#facts (Proof.goal state))
1.32 - in
1.33 - one_line_proof_text ctxt num_chained one_line_params
1.34 - end,
1.35 + message = fn play =>
1.36 + let
1.37 + val ctxt = Proof.context_of state
1.38 + val (_, override_params) = extract_proof_method params meth
1.39 + val one_line_params =
1.40 + (play, proof_banner mode name, used_facts, minimize_command override_params name,
1.41 + subgoal, subgoal_count)
1.42 + val num_chained = length (#facts (Proof.goal state))
1.43 + in
1.44 + one_line_proof_text ctxt num_chained one_line_params
1.45 + end,
1.46 message_tail = ""}
1.47 | play =>
1.48 let
1.49 @@ -128,10 +127,7 @@
1.50 fun n_facts names =
1.51 let val n = length names in
1.52 string_of_int n ^ " fact" ^ plural_s n ^
1.53 - (if n > 0 then
1.54 - ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
1.55 - else
1.56 - "")
1.57 + (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
1.58 end
1.59
1.60 fun print silent f = if silent then () else Output.urgent_message (f ())
1.61 @@ -141,10 +137,9 @@
1.62 smt_proofs, preplay_timeout, ...} : params)
1.63 silent (prover : prover) timeout i n state goal facts =
1.64 let
1.65 - val _ =
1.66 - print silent (fn () =>
1.67 - "Testing " ^ n_facts (map fst facts) ^
1.68 - (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
1.69 + val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
1.70 + (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
1.71 +
1.72 val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
1.73 val params =
1.74 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
1.75 @@ -230,7 +225,7 @@
1.76 (case test timeout (sup @ r0) of
1.77 result as {outcome = NONE, used_facts, ...} =>
1.78 min depth result (filter_used_facts true used_facts sup)
1.79 - (filter_used_facts true used_facts r0)
1.80 + (filter_used_facts true used_facts r0)
1.81 | _ =>
1.82 let
1.83 val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
1.84 @@ -259,8 +254,8 @@
1.85 val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
1.86 fun test timeout = test_facts params silent prover timeout i n state goal
1.87 val (chained, non_chained) = List.partition is_fact_chained facts
1.88 - (* Push chained facts to the back, so that they are less likely to be
1.89 - kicked out by the linear minimization algorithm. *)
1.90 + (* Push chained facts to the back, so that they are less likely to be kicked out by the linear
1.91 + minimization algorithm. *)
1.92 val facts = non_chained @ chained
1.93 in
1.94 (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
1.95 @@ -378,8 +373,7 @@
1.96 | NONE => result)
1.97 end
1.98
1.99 -fun get_minimizing_prover ctxt mode do_learn name params minimize_command
1.100 - problem =
1.101 +fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem =
1.102 get_prover ctxt mode name params minimize_command problem
1.103 |> maybe_minimize ctxt mode do_learn name params problem
1.104
1.105 @@ -393,14 +387,14 @@
1.106 in
1.107 (case subgoal_count state of
1.108 0 => Output.urgent_message "No subgoal!"
1.109 - | n => (case provers of
1.110 - [] => error "No prover is set."
1.111 - | prover :: _ =>
1.112 - (kill_provers ();
1.113 - minimize_facts do_learn prover params false i n state goal NONE facts
1.114 - |> (fn (_, (preplay, message, message_tail)) =>
1.115 - message (Lazy.force preplay) ^ message_tail
1.116 - |> Output.urgent_message))))
1.117 + | n =>
1.118 + (case provers of
1.119 + [] => error "No prover is set."
1.120 + | prover :: _ =>
1.121 + (kill_provers ();
1.122 + minimize_facts do_learn prover params false i n state goal NONE facts
1.123 + |> (fn (_, (preplay, message, message_tail)) =>
1.124 + Output.urgent_message (message (Lazy.force preplay) ^ message_tail)))))
1.125 end
1.126
1.127 end;