# HG changeset patch # User wenzelm # Date 1376732090 -7200 # Node ID 8dceafa07c4fb959ccb18fa53518db9021ac8612 # Parent cba2ddfb30c47192ecfbb531494a423125a1bb8b more explicit sendback propertries based on mode; diff -r cba2ddfb30c4 -r 8dceafa07c4f src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Fri Aug 16 23:11:51 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Sat Aug 17 11:34:50 2013 +0200 @@ -13,7 +13,7 @@ val string_of_reconstructor : reconstructor -> string - val one_line_proof_text : bool -> int -> one_line_params -> string + val one_line_proof_text : Properties.T -> int -> one_line_params -> string val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string @@ -71,25 +71,23 @@ using_labels ls ^ apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss -fun try_command_line auto banner time command = +fun try_command_line sendback_props banner time command = banner ^ ": " ^ - Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^ + Active.sendback_markup sendback_props command ^ show_time time ^ "." fun minimize_line _ _ [] = "" - | minimize_line auto minimize_command ss = + | minimize_line sendback_props minimize_command ss = case minimize_command ss of "" => "" | command => - "\nTo minimize: " ^ - Active.sendback_markup (if auto then [Markup.padding_command] else []) - command ^ "." + "\nTo minimize: " ^ Active.sendback_markup sendback_props command ^ "." fun split_used_facts facts = facts |> List.partition (fn (_, (sc, _)) => sc = Chained) |> pairself (sort_distinct (string_ord o pairself fst)) -fun one_line_proof_text auto num_chained +fun one_line_proof_text sendback_props num_chained (preplay, banner, used_facts, minimize_command, subgoal, subgoal_count) = let @@ -113,8 +111,8 @@ ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \ \solve this.)" else - try_command_line auto banner ext_time) - in try_line ^ minimize_line auto minimize_command (map fst (extra @ chained)) end + try_command_line sendback_props banner ext_time) + in try_line ^ minimize_line sendback_props minimize_command (map fst (extra @ chained)) end diff -r cba2ddfb30c4 -r 8dceafa07c4f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Aug 16 23:11:51 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Aug 17 11:34:50 2013 +0200 @@ -464,6 +464,11 @@ | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this" +fun sendback_properties mode = + if mode = Auto_Try orelse mode = Normal_Result + then [Markup.padding_command] + else [] + fun bunch_of_reconstructors needs_full_types lam_trans = if needs_full_types then [Metis (full_type_enc, lam_trans false), @@ -696,6 +701,7 @@ let val thy = Proof.theory_of state val ctxt = Proof.context_of state + val sendback_props = sendback_properties mode val atp_mode = if Config.get ctxt completish then Sledgehammer_Completish else Sledgehammer @@ -976,7 +982,7 @@ subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - proof_text ctxt (mode = Auto_Try) isar_proofs isar_params + proof_text ctxt sendback_props isar_proofs isar_params num_chained one_line_params end, (if verbose then @@ -1154,6 +1160,7 @@ ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let val ctxt = Proof.context_of state + val sendback_props = sendback_properties mode fun weight_facts facts = let val num_facts = length facts in facts ~~ (0 upto num_facts - 1) @@ -1181,7 +1188,7 @@ subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - one_line_proof_text (mode = Auto_Try) num_chained one_line_params + one_line_proof_text sendback_props num_chained one_line_params end, if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." @@ -1202,6 +1209,7 @@ ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) = let + val sendback_props = sendback_properties mode val reconstr = if name = metisN then Metis (type_enc |> the_default (hd partial_type_encs), @@ -1228,7 +1236,7 @@ subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - one_line_proof_text (mode = Auto_Try) num_chained one_line_params + one_line_proof_text sendback_props num_chained one_line_params end, message_tail = ""} | play => diff -r cba2ddfb30c4 -r 8dceafa07c4f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Aug 16 23:11:51 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Aug 17 11:34:50 2013 +0200 @@ -25,9 +25,9 @@ Proof.context -> (string * stature) list vector -> 'a proof -> string list option val isar_proof_text : - Proof.context -> bool -> bool option -> isar_params -> one_line_params -> string + Proof.context -> Properties.T -> bool option -> isar_params -> one_line_params -> string val proof_text : - Proof.context -> bool -> bool option -> isar_params -> int -> one_line_params + Proof.context -> Properties.T -> bool option -> isar_params -> int -> one_line_params -> string end; @@ -412,7 +412,7 @@ * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table * string proof * thm -fun isar_proof_text ctxt auto isar_proofs +fun isar_proof_text ctxt sendback_props isar_proofs (debug, verbose, preplay_timeout, preplay_trace, isar_compress, isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof, goal) @@ -425,7 +425,7 @@ |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes) - val one_line_proof = one_line_proof_text auto 0 one_line_params + val one_line_proof = one_line_proof_text sendback_props 0 one_line_params val type_enc = if is_typed_helper_used_in_atp_proof atp_proof then full_typesN else partial_typesN @@ -625,7 +625,7 @@ "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ - Active.sendback_markup (if auto then [Markup.padding_command] else []) isar_text + Active.sendback_markup sendback_props isar_text end end val isar_proof = @@ -645,12 +645,12 @@ | Trust_Playable _ => true | Failed_to_Play _ => true -fun proof_text ctxt auto isar_proofs isar_params num_chained +fun proof_text ctxt sendback_props isar_proofs isar_params num_chained (one_line_params as (preplay, _, _, _, _, _)) = (if isar_proofs = SOME true orelse (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then - isar_proof_text ctxt auto isar_proofs isar_params + isar_proof_text ctxt sendback_props isar_proofs isar_params else - one_line_proof_text auto num_chained) one_line_params + one_line_proof_text sendback_props num_chained) one_line_params end;