--- 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
--- 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"
--- 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
--- 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;
--- 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;
--- 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. *)
--- 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)
--- 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. *)