# HG changeset patch # User blanchet # Date 1391180840 -3600 # Node ID 5d027af93a08d69c0a0de5ddadea25ba1de48712 # Parent d1e3b708d74bb2ff7f47d6d1a92f45640b9cf065 moved ML code around diff -r d1e3b708d74b -r 5d027af93a08 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jan 31 14:33:02 2014 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jan 31 16:07:20 2014 +0100 @@ -70,7 +70,6 @@ val value = AList.lookup (op =) args key in if is_some value then (label, the value) :: list else list end - datatype sh_data = ShData of { calls: int, success: int, @@ -131,7 +130,6 @@ proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns) - datatype reconstructor_mode = Unminimized | Minimized | UnminimizedFT | MinimizedFT @@ -349,8 +347,7 @@ end - -(* Warning: we implicitly assume single-threaded execution here! *) +(* Warning: we implicitly assume single-threaded execution here *) val data = Unsynchronized.ref ([] : (int * data) list) fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy) @@ -496,9 +493,9 @@ val time_prover = run_time |> Time.toMilliseconds val msg = message (Lazy.force preplay) ^ message_tail in - case outcome of + (case outcome of NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) - | SOME _ => (msg, SH_FAIL (time_isa, time_prover)) + | SOME _ => (msg, SH_FAIL (time_isa, time_prover))) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) @@ -508,7 +505,6 @@ ({pre=st, log, pos, ...}: Mirabelle.run_args) = let val thy = Proof.theory_of st - val ctxt = Proof.context_of st val triv_str = if trivial then "[T] " else "" val _ = change_data id inc_sh_calls val _ = if trivial then () else change_data id inc_sh_nontriv_calls @@ -517,11 +513,12 @@ val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default val strict = AList.lookup (op =) args strictK |> the_default strict_default val max_facts = - case AList.lookup (op =) args max_factsK of + (case AList.lookup (op =) args max_factsK of SOME max => max - | NONE => case AList.lookup (op =) args max_relevantK of - SOME max => max - | NONE => max_facts_default + | NONE => + (case AList.lookup (op =) args max_relevantK of + SOME max => max + | NONE => max_facts_default)) val slice = AList.lookup (op =) args sliceK |> the_default slice_default val lam_trans = AList.lookup (op =) args lam_transK val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK @@ -546,7 +543,7 @@ hard_timeout timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st in - case result of + (case result of SH_OK (time_isa, time_prover, names) => let fun get_thms (name, stature) = @@ -570,16 +567,14 @@ val _ = change_data id (inc_sh_time_isa time_isa) val _ = change_data id (inc_sh_time_prover_fail time_prover) in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end - | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg) + | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)) end end -fun run_minimize args reconstructor named_thms id - ({pre=st, log, ...}: Mirabelle.run_args) = +fun run_minimize args reconstructor named_thms id ({pre = st, log, ...} : Mirabelle.run_args) = let val thy = Proof.theory_of st - val ctxt = Proof.context_of st val {goal, ...} = Proof.goal st val n0 = length (these (!named_thms)) val prover_name = get_prover_name thy args @@ -613,7 +608,7 @@ minimize st goal NONE (these (!named_thms)) val msg = message (Lazy.force preplay) ^ message_tail in - case used_facts of + (case used_facts of SOME named_thms' => (change_data id inc_min_succs; change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); @@ -623,7 +618,7 @@ named_thms := SOME named_thms'; log (minimize_tag id ^ "succeeded:\n" ^ msg)) ) - | NONE => log (minimize_tag id ^ "failed: " ^ msg) + | NONE => log (minimize_tag id ^ "failed: " ^ msg)) end fun override_params prover type_enc timeout = @@ -649,8 +644,7 @@ timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal fun sledge_tac time_slice prover type_enc = Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt - (override_params prover type_enc (my_timeout time_slice)) - fact_override + (override_params prover type_enc (my_timeout time_slice)) fact_override in if !reconstructor = "sledgehammer_tac" then sledge_tac 0.2 ATP_Systems.vampireN "mono_native" @@ -674,8 +668,7 @@ ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end else if !reconstructor = "metis" then - Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt - thms + Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else K all_tac end @@ -689,19 +682,16 @@ change_data id (inc_reconstructor_lemmas m (length named_thms)); change_data id (inc_reconstructor_time m t); change_data id (inc_reconstructor_posns m (pos, trivial)); - if name = "proof" then change_data id (inc_reconstructor_proofs m) - else (); + if name = "proof" then change_data id (inc_reconstructor_proofs m) else (); "succeeded (" ^ string_of_int t ^ ")") fun timed_reconstructor named_thms = (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true) - handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); - ("timeout", false)) + handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false)) | ERROR msg => ("error: " ^ msg, false) val _ = log separator val _ = change_data id (inc_reconstructor_calls m) - val _ = if trivial then () - else change_data id (inc_reconstructor_nontriv_calls m) + val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m) in named_thms |> timed_reconstructor diff -r d1e3b708d74b -r 5d027af93a08 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Jan 31 14:33:02 2014 +0100 +++ b/src/HOL/Sledgehammer.thy Fri Jan 31 16:07:20 2014 +0100 @@ -18,9 +18,8 @@ ML_file "Tools/Sledgehammer/sledgehammer_util.ML" ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML" +ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML" ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML" -ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML" -ML_file "Tools/Sledgehammer/sledgehammer_isar_print.ML" ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML" ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML" ML_file "Tools/Sledgehammer/sledgehammer_isar_try0.ML" diff -r d1e3b708d74b -r 5d027af93a08 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 14:33:02 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 16:07:20 2014 +0100 @@ -32,7 +32,6 @@ open Sledgehammer_Reconstructor open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Annotate -open Sledgehammer_Isar_Print open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Compress open Sledgehammer_Isar_Try0 diff -r d1e3b708d74b -r 5d027af93a08 src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML Fri Jan 31 14:33:02 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,262 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML - Author: Jasmin Blanchette, TU Muenchen - Author: Steffen Juilf Smolka, TU Muenchen - -Basic mapping from proof data structures to proof strings. -*) - -signature SLEDGEHAMMER_ISAR_PRINT = -sig - type isar_proof = Sledgehammer_Isar_Proof.isar_proof - type reconstructor = Sledgehammer_Reconstructor.reconstructor - type one_line_params = Sledgehammer_Reconstructor.one_line_params - - val string_of_reconstructor : reconstructor -> string - val one_line_proof_text : int -> one_line_params -> string - val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string -end; - -structure Sledgehammer_Isar_Print : SLEDGEHAMMER_ISAR_PRINT = -struct - -open ATP_Util -open ATP_Proof -open ATP_Problem_Generate -open ATP_Proof_Reconstruct -open Sledgehammer_Util -open Sledgehammer_Reconstructor -open Sledgehammer_Isar_Proof -open Sledgehammer_Isar_Annotate - - -(** reconstructors **) - -fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans - | string_of_reconstructor SMT = smtN - - -(** one-liner reconstructor proofs **) - -fun show_time NONE = "" - | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")" - -(* FIXME: Various bugs, esp. with "unfolding" -fun unusing_chained_facts _ 0 = "" - | unusing_chained_facts used_chaineds num_chained = - if length used_chaineds = num_chained then "" - else if null used_chaineds then "(* using no facts *) " - else "(* using only " ^ space_implode " " used_chaineds ^ " *) " -*) - -fun apply_on_subgoal _ 1 = "by " - | apply_on_subgoal 1 _ = "apply " - | apply_on_subgoal i n = - "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n - -fun using_labels [] = "" - | using_labels ls = "using " ^ space_implode " " (map string_of_label ls) ^ " " - -fun command_call name [] = - name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" - | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" - -fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) = - (* unusing_chained_facts used_chaineds num_chained ^ *) - using_labels ls ^ apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss - -fun try_command_line banner time command = - banner ^ ": " ^ - Active.sendback_markup [Markup.padding_command] command ^ - show_time time ^ "." - -fun minimize_line _ [] = "" - | minimize_line minimize_command ss = - (case minimize_command ss of - "" => "" - | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] 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 num_chained - ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = - let - val (chained, extra) = split_used_facts used_facts - val (failed, ext_time) = - (case play of - Played time => (false, (SOME (false, time))) - | Play_Timed_Out time => (false, SOME (true, time)) - | Play_Failed => (true, NONE) - | Not_Played => (false, NONE)) - val try_line = - ([], map fst extra) - |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained - |> (if failed then - enclose "One-line proof reconstruction failed: " - ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \ - \solve this.)" - else - try_command_line banner ext_time) - in - try_line ^ minimize_line minimize_command (map fst (extra @ chained)) - end - - -(** detailed Isar proofs **) - -val indent_size = 2 - -fun string_of_proof ctxt type_enc lam_trans i n proof = - let - (* Make sure only type constraints inserted by the type annotation code are printed. *) - val ctxt = - ctxt |> Config.put show_markup false - |> Config.put Printer.show_type_emphasis false - |> Config.put show_types false - |> Config.put show_sorts false - |> Config.put show_consts false - - val register_fixes = map Free #> fold Variable.auto_fixes - - fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt) - - fun of_indent ind = replicate_string (ind * indent_size) " " - fun of_moreover ind = of_indent ind ^ "moreover\n" - fun of_label l = if l = no_label then "" else string_of_label l ^ ": " - - fun of_obtain qs nr = - (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then - "ultimately " - else if nr = 1 orelse member (op =) qs Then then - "then " - else - "") ^ "obtain" - - fun of_show_have qs = if member (op =) qs Show then "show" else "have" - fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence" - - fun of_have qs nr = - if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then - "ultimately " ^ of_show_have qs - else if nr = 1 orelse member (op =) qs Then then - of_thus_hence qs - else - of_show_have qs - - fun add_term term (s, ctxt) = - (s ^ (term - |> singleton (Syntax.uncheck_terms ctxt) - |> annotate_types ctxt - |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of) - |> simplify_spaces - |> maybe_quote), - ctxt |> Variable.auto_fixes term) - - fun by_method meth = "by " ^ - (case meth of - Simp_Method => "simp" - | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)" - | Auto_Method => "auto" - | Fastforce_Method => "fastforce" - | Force_Method => "force" - | Arith_Method => "arith" - | Blast_Method => "blast" - | Meson_Method => "meson" - | _ => raise Fail "Sledgehammer_Isar_Print: by_method") - - fun with_facts none _ [] [] = none - | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss)) - - val using_facts = with_facts "" (enclose "using " " ") - - (* Local facts are always passed via "using", which affects "meson" and "metis". This is - arguably stylistically superior, because it emphasises the structure of the proof. It is also - more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence" - and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) - fun of_method ls ss Metis_Method = - using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ([], ss) - | of_method ls ss Meson_Method = - using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss - | of_method ls ss meth = using_facts ls ss ^ by_method meth - - fun of_byline ind (ls, ss) meth = - let - val ls = ls |> sort_distinct label_ord - val ss = ss |> sort_distinct string_ord - in - "\n" ^ of_indent (ind + 1) ^ of_method ls ss meth - end - - fun of_free (s, T) = - maybe_quote s ^ " :: " ^ - maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T)) - - fun add_frees xs (s, ctxt) = - (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs) - - fun add_fix _ [] = I - | add_fix ind xs = - add_suffix (of_indent ind ^ "fix ") - #> add_frees xs - #> add_suffix "\n" - - fun add_assm ind (l, t) = - add_suffix (of_indent ind ^ "assume " ^ of_label l) - #> add_term t - #> add_suffix "\n" - - fun add_assms ind assms = fold (add_assm ind) assms - - fun add_step_post ind l t facts meth = - add_suffix (of_label l) - #> add_term t - #> add_suffix (of_byline ind facts meth ^ "\n") - - fun of_subproof ind ctxt proof = - let - val ind = ind + 1 - val s = of_proof ind ctxt proof - val prefix = "{ " - val suffix = " }" - in - replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ - String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^ - suffix ^ "\n" - end - and of_subproofs _ _ _ [] = "" - | of_subproofs ind ctxt qs subproofs = - (if member (op =) qs Then then of_moreover ind else "") ^ - space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs) - and add_step_pre ind qs subproofs (s, ctxt) = - (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt) - and add_step ind (Let (t1, t2)) = - add_suffix (of_indent ind ^ "let ") - #> add_term t1 - #> add_suffix " = " - #> add_term t2 - #> add_suffix "\n" - | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) = - add_step_pre ind qs subproofs - #> (case xs of - [] => add_suffix (of_have qs (length subproofs) ^ " ") - | _ => - add_suffix (of_obtain qs (length subproofs) ^ " ") - #> add_frees xs - #> add_suffix " where ") - #> add_step_post ind l t facts meth - and add_steps ind = fold (add_step ind) - and of_proof ind ctxt (Proof (xs, assms, steps)) = - ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst - in - (* One-step Metis proofs are pointless; better use the one-liner directly. *) - (case proof of - Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *) - | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => "" - | _ => - (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ - of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ - of_indent 0 ^ (if n <> 1 then "next" else "qed")) - end - -end; diff -r d1e3b708d74b -r 5d027af93a08 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 14:33:02 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 16:07:20 2014 +0100 @@ -52,11 +52,21 @@ val relabel_proof_canonically : isar_proof -> isar_proof structure Canonical_Lbl_Tab : TABLE + + val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string end; structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF = struct +open ATP_Util +open ATP_Proof +open ATP_Problem_Generate +open ATP_Proof_Reconstruct +open Sledgehammer_Util +open Sledgehammer_Reconstructor +open Sledgehammer_Isar_Annotate + type label = string * int type facts = label list * string list (* local and global facts *) @@ -110,9 +120,7 @@ val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) - -(** canonical proof labels: 1, 2, 3, ... in post traversal order **) - +(* canonical proof labels: 1, 2, 3, ... in post traversal order *) fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2) structure Canonical_Lbl_Tab = Table( @@ -154,4 +162,152 @@ fst (do_proof proof (0, [])) end +val indent_size = 2 + +fun string_of_proof ctxt type_enc lam_trans i n proof = + let + (* Make sure only type constraints inserted by the type annotation code are printed. *) + val ctxt = + ctxt |> Config.put show_markup false + |> Config.put Printer.show_type_emphasis false + |> Config.put show_types false + |> Config.put show_sorts false + |> Config.put show_consts false + + val register_fixes = map Free #> fold Variable.auto_fixes + + fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt) + + fun of_indent ind = replicate_string (ind * indent_size) " " + fun of_moreover ind = of_indent ind ^ "moreover\n" + fun of_label l = if l = no_label then "" else string_of_label l ^ ": " + + fun of_obtain qs nr = + (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " + else if nr = 1 orelse member (op =) qs Then then "then " + else "") ^ "obtain" + + fun of_show_have qs = if member (op =) qs Show then "show" else "have" + fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence" + + fun of_have qs nr = + if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs + else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs + else of_show_have qs + + fun add_term term (s, ctxt) = + (s ^ (term + |> singleton (Syntax.uncheck_terms ctxt) + |> annotate_types ctxt + |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of) + |> simplify_spaces + |> maybe_quote), + ctxt |> Variable.auto_fixes term) + + fun by_method meth = "by " ^ + (case meth of + Simp_Method => "simp" + | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)" + | Auto_Method => "auto" + | Fastforce_Method => "fastforce" + | Force_Method => "force" + | Arith_Method => "arith" + | Blast_Method => "blast" + | Meson_Method => "meson" + | _ => raise Fail "Sledgehammer_Isar_Print: by_method") + + fun with_facts none _ [] [] = none + | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss)) + + val using_facts = with_facts "" (enclose "using " " ") + + (* Local facts are always passed via "using", which affects "meson" and "metis". This is + arguably stylistically superior, because it emphasises the structure of the proof. It is also + more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence" + and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) + fun of_method ls ss Metis_Method = + using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ss + | of_method ls ss Meson_Method = + using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss + | of_method ls ss meth = using_facts ls ss ^ by_method meth + + fun of_byline ind (ls, ss) meth = + let + val ls = ls |> sort_distinct label_ord + val ss = ss |> sort_distinct string_ord + in + "\n" ^ of_indent (ind + 1) ^ of_method ls ss meth + end + + fun of_free (s, T) = + maybe_quote s ^ " :: " ^ + maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T)) + + fun add_frees xs (s, ctxt) = + (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs) + + fun add_fix _ [] = I + | add_fix ind xs = + add_suffix (of_indent ind ^ "fix ") + #> add_frees xs + #> add_suffix "\n" + + fun add_assm ind (l, t) = + add_suffix (of_indent ind ^ "assume " ^ of_label l) + #> add_term t + #> add_suffix "\n" + + fun add_assms ind assms = fold (add_assm ind) assms + + fun add_step_post ind l t facts meth = + add_suffix (of_label l) + #> add_term t + #> add_suffix (of_byline ind facts meth ^ "\n") + + fun of_subproof ind ctxt proof = + let + val ind = ind + 1 + val s = of_proof ind ctxt proof + val prefix = "{ " + val suffix = " }" + in + replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ + String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^ + suffix ^ "\n" + end + and of_subproofs _ _ _ [] = "" + | of_subproofs ind ctxt qs subproofs = + (if member (op =) qs Then then of_moreover ind else "") ^ + space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs) + and add_step_pre ind qs subproofs (s, ctxt) = + (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt) + and add_step ind (Let (t1, t2)) = + add_suffix (of_indent ind ^ "let ") + #> add_term t1 + #> add_suffix " = " + #> add_term t2 + #> add_suffix "\n" + | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) = + add_step_pre ind qs subproofs + #> (case xs of + [] => add_suffix (of_have qs (length subproofs) ^ " ") + | _ => + add_suffix (of_obtain qs (length subproofs) ^ " ") + #> add_frees xs + #> add_suffix " where ") + #> add_step_post ind l t facts meth + and add_steps ind = fold (add_step ind) + and of_proof ind ctxt (Proof (xs, assms, steps)) = + ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst + in + (* One-step Metis proofs are pointless; better use the one-liner directly. *) + (case proof of + Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *) + | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => "" + | _ => + (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ + of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ + of_indent 0 ^ (if n <> 1 then "next" else "qed")) + end + end; diff -r d1e3b708d74b -r 5d027af93a08 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jan 31 14:33:02 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jan 31 16:07:20 2014 +0100 @@ -110,7 +110,6 @@ open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Reconstructor -open Sledgehammer_Isar_Print open Sledgehammer_Isar (* Empty string means create files in Isabelle's temporary files directory. *) diff -r d1e3b708d74b -r 5d027af93a08 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Jan 31 14:33:02 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Jan 31 16:07:20 2014 +0100 @@ -42,7 +42,6 @@ open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Reconstructor -open Sledgehammer_Isar_Print open Sledgehammer_Prover val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true) diff -r d1e3b708d74b -r 5d027af93a08 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Fri Jan 31 14:33:02 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Fri Jan 31 16:07:20 2014 +0100 @@ -19,13 +19,16 @@ Play_Failed | Not_Played - val string_of_play_outcome: play_outcome -> string - type minimize_command = string list -> string type one_line_params = (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int val smtN : string + val string_of_reconstructor : reconstructor -> string + val string_of_play_outcome : play_outcome -> string + val reconstructor_command : reconstructor -> int -> int -> string list -> int -> string list -> + string + val one_line_proof_text : int -> one_line_params -> string val silence_reconstructors : bool -> Proof.context -> Proof.context end; @@ -35,6 +38,7 @@ open ATP_Util open ATP_Problem_Generate +open ATP_Proof_Reconstruct datatype reconstructor = Metis of string * string | @@ -46,16 +50,81 @@ Play_Failed | Not_Played +type minimize_command = string list -> string +type one_line_params = + (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int + +val smtN = "smt" + +fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans + | string_of_reconstructor SMT = smtN + fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out" | string_of_play_outcome Play_Failed = "failed" | string_of_play_outcome _ = "unknown" -type minimize_command = string list -> string -type one_line_params = - (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int +(* FIXME: Various bugs, esp. with "unfolding" +fun unusing_chained_facts _ 0 = "" + | unusing_chained_facts used_chaineds num_chained = + if length used_chaineds = num_chained then "" + else if null used_chaineds then "(* using no facts *) " + else "(* using only " ^ space_implode " " used_chaineds ^ " *) " +*) + +fun apply_on_subgoal _ 1 = "by " + | apply_on_subgoal 1 _ = "apply " + | apply_on_subgoal i n = + "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n + +fun command_call name [] = + name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" + | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" + +fun reconstructor_command reconstr i n used_chaineds num_chained ss = + (* unusing_chained_facts used_chaineds num_chained ^ *) + apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss + +fun show_time NONE = "" + | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")" + +fun try_command_line banner time command = + banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ show_time time ^ "." -val smtN = "smt" +fun minimize_line _ [] = "" + | minimize_line minimize_command ss = + (case minimize_command ss of + "" => "" + | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] 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 num_chained + ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = + let + val (chained, extra) = split_used_facts used_facts + + val (failed, ext_time) = + (case play of + Played time => (false, (SOME (false, time))) + | Play_Timed_Out time => (false, SOME (true, time)) + | Play_Failed => (true, NONE) + | Not_Played => (false, NONE)) + + val try_line = + map fst extra + |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained + |> (if failed then + enclose "One-line proof reconstruction failed: " + ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)" + else + try_command_line banner ext_time) + in + try_line ^ minimize_line minimize_command (map fst (extra @ chained)) + end (* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification bound exceeded" warnings and the like. *)