--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 19:32:13 2014 +0100
@@ -13,6 +13,8 @@
type stature = ATP_Problem_Generate.stature
type one_line_params = Sledgehammer_Reconstructor.one_line_params
+ val trace : bool Config.T
+
type isar_params =
bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
@@ -42,6 +44,8 @@
open String_Redirect
+val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
+
val e_skolemize_rules = ["skolemize", "shift_quantors"]
val spass_pirate_datatype_rule = "DT"
val vampire_skolemisation_rule = "skolemisation"
@@ -103,99 +107,16 @@
add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
end
-val add_labels_of_proof =
- steps_of_proof
- #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
-
-fun kill_useless_labels_in_proof proof =
- let
- val used_ls = add_labels_of_proof proof []
-
- fun kill_label l = if member (op =) used_ls l then l else no_label
- fun kill_assms assms = map (apfst kill_label) assms
-
- fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
- Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
- | kill_step step = step
- and kill_proof (Proof (fix, assms, steps)) =
- Proof (fix, kill_assms assms, map kill_step steps)
- in
- kill_proof proof
- end
-
-val assume_prefix = "a"
-val have_prefix = "f"
-
-val relabel_proof =
- let
- fun fresh_label depth prefix (accum as (l, subst, next)) =
- if l = no_label then
- accum
- else
- let val l' = (replicate_string (depth + 1) prefix, next) in
- (l', (l, l') :: subst, next + 1)
- end
-
- fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
-
- fun relabel_assm depth (l, t) (subst, next) =
- let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
- ((l, t), (subst, next))
- end
-
- fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
-
- fun relabel_steps _ _ _ [] = []
- | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
- let
- val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
- val sub = relabel_proofs subst depth sub
- val by = apfst (relabel_facts subst) by
- in
- Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
- end
- | relabel_steps subst depth next (step :: steps) =
- step :: relabel_steps subst depth next steps
- and relabel_proof subst depth (Proof (fix, assms, steps)) =
- let val (assms, subst) = relabel_assms subst depth assms in
- Proof (fix, assms, relabel_steps subst depth 1 steps)
- end
- and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
- in
- relabel_proof [] 0
- end
-
-val chain_direct_proof =
- let
- fun chain_qs_lfs NONE lfs = ([], lfs)
- | chain_qs_lfs (SOME l0) lfs =
- if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
- fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
- let val (qs', lfs) = chain_qs_lfs lbl lfs in
- Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss))
- end
- | chain_step _ step = step
- and chain_steps _ [] = []
- | chain_steps (prev as SOME _) (i :: is) =
- chain_step prev i :: chain_steps (label_of_step i) is
- | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
- and chain_proof (Proof (fix, assms, steps)) =
- Proof (fix, assms, chain_steps (try (List.last #> fst) assms) steps)
- and chain_proofs proofs = map (chain_proof) proofs
- in
- chain_proof
- end
-
type isar_params =
bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
val arith_methodss =
[[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
- Metis_Method], [Meson_Method]]
-val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
+ Algebra_Method], [Metis_Method], [Meson_Method]]
+val datatype_methodss = [[Simp_Method], [Simp_Size_Method]]
val metislike_methodss =
[[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
- Force_Method], [Meson_Method]]
+ Force_Method, Algebra_Method], [Meson_Method]]
val rewrite_methodss =
[[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
@@ -345,7 +266,7 @@
val string_of_isar_proof =
string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count
- val trace = false
+ val trace = Config.get ctxt trace
val isar_proof =
refute_graph
@@ -356,13 +277,21 @@
|> postprocess_isar_proof_remove_unreferenced_steps I
|> relabel_isar_proof_canonically
- val preplay_data as {overall_preplay_outcome, ...} =
+ val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
preplay_timeout isar_proof
+ fun str_of_preplay_outcome outcome =
+ if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
+
+ fun str_of_meth l meth =
+ string_of_proof_method meth ^ " " ^ str_of_preplay_outcome (preplay_outcome l meth)
+ fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
+
fun trace_isar_proof label proof =
if trace then
- tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof proof ^ "\n")
+ tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
+ "\n")
else
()
@@ -378,9 +307,11 @@
(try0_isar ? minimize_isar_step_dependencies preplay_data)
|> tap (trace_isar_proof "Minimized")
|> `overall_preplay_outcome
- ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
+ ||> chain_isar_proof
+ ||> kill_useless_labels_in_isar_proof
+ ||> relabel_isar_proof_finally
in
- (case string_of_isar_proof isar_proof of
+ (case string_of_isar_proof (K (K "")) isar_proof of
"" =>
if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
else ""
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 19:32:13 2014 +0100
@@ -79,14 +79,15 @@
| _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
end
-(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
+(* Tries merging the first step into the second step.
+ FIXME: Arbitrarily picks the second step's method. *)
fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
- (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
+ (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), methss2))) =
let
val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
val gfs = union (op =) gfs1 gfs2
in
- SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
+ SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), methss2)))
end
| try_merge _ _ = NONE
@@ -96,7 +97,7 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
fun compress_isar_proof compress_isar
- ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
+ ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
if compress_isar <= 1.0 then
proof
else
@@ -136,57 +137,55 @@
(** elimination of trivial, one-step subproofs **)
- fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
+ fun elim_subproofs' time qs fix l t lfs gfs (methss as (meth :: _) :: _) subs nontriv_subs =
if null subs orelse not (compress_further ()) then
- (set_preplay_outcome l (Played time);
- Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
+ (set_preplay_outcome l meth (Played time);
+ Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), methss)))
else
(case subs of
(sub as Proof (_, assms, sub_steps)) :: subs =>
(let
- (* trivial subproofs have exactly one Prove step *)
- val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
+ (* trivial subproofs have exactly one "Prove" step *)
+ val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), (meth' :: _) :: _))) =
+ try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
- val Played time' = get_preplay_outcome l'
+ val Played time' = Lazy.force (preplay_outcome l' meth')
(* merge steps *)
val subs'' = subs @ nontriv_subs
- val lfs'' =
- subtract (op =) (map fst assms) lfs'
- |> union (op =) lfs
+ val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
val gfs'' = union (op =) gfs' gfs
- val by = ((lfs'', gfs''), meth)
+ val by = ((lfs'', gfs''), methss(*FIXME*))
val step'' = Prove (qs, fix, l, t, subs'', by)
(* check if the modified step can be preplayed fast enough *)
val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
val Played time'' = preplay_quietly timeout step''
-
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
- elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs
+ elim_subproofs' time'' qs fix l t lfs'' gfs'' methss subs nontriv_subs
end
handle Bind =>
- elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs))
+ elim_subproofs' time qs fix l t lfs gfs methss subs (sub :: nontriv_subs))
| _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
fun elim_subproofs (step as Let _) = step
- | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+ | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
+ ((lfs, gfs), methss as (meth :: _) :: _))) =
if subproofs = [] then
step
else
- (case get_preplay_outcome l of
- Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+ (case Lazy.force (preplay_outcome l meth) of
+ Played time => elim_subproofs' time qs fix l t lfs gfs methss subproofs []
| _ => step)
(** top_level compression: eliminate steps by merging them into their successors **)
-
fun compress_top_level steps =
let
(* (#successors, (size_of_term t, position)) *)
- fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i))
+ fun cand_key (i, l, t_size) = (length (get_successors l), (t_size, i))
val compression_ord =
prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
@@ -207,33 +206,36 @@
| add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
in
(steps
- |> split_last |> fst (* keep last step *)
- |> fold_index add_cand) []
+ |> split_last |> fst (* keep last step *)
+ |> fold_index add_cand) []
end
fun try_eliminate (i, l, _) succ_lbls steps =
let
+ val ((cand as Prove (_, _, l, _, _, ((lfs, _), (meth :: _) :: _))) :: steps') =
+ drop i steps
+
+ val succs = collect_successors steps' succ_lbls
+ val succ_meths = map (hd o hd o snd o the o byline_of_isar_step) succs
+
(* only touch steps that can be preplayed successfully *)
- val Played time = get_preplay_outcome l
+ val Played time = Lazy.force (preplay_outcome l meth)
+
+ val succs' = map (try_merge cand #> the) succs
val succ_times =
- map (get_preplay_outcome #> (fn Played t => t)) succ_lbls
+ map2 ((fn Played t => t) o Lazy.force oo preplay_outcome) succ_lbls succ_meths
val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
val timeouts =
map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
- val ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps
-
(* FIXME: debugging *)
val _ =
- if the (label_of_step cand) <> l then
+ if the (label_of_isar_step cand) <> l then
raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
else
()
- val succs = collect_successors steps' succ_lbls
- val succs' = map (try_merge cand #> the) succs
-
(* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
val play_outcomes = map2 preplay_quietly timeouts succs'
@@ -245,7 +247,7 @@
val steps2 = update_steps steps2 succs'
in
decrement_step_count (); (* candidate successfully eliminated *)
- map2 set_preplay_outcome succ_lbls play_outcomes;
+ map3 set_preplay_outcome succ_lbls succ_meths play_outcomes;
map (replace_successor l succ_lbls) lfs;
(* removing the step would mess up the indices -> replace with dummy step instead *)
steps1 @ dummy_isar_step :: steps2
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 19:32:13 2014 +0100
@@ -26,12 +26,12 @@
val slack = seconds 0.1
fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
- | minimize_isar_step_dependencies {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
- (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
- (case get_preplay_outcome l of
+ | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
+ (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) =
+ (case Lazy.force (preplay_outcome l meth) of
Played time =>
let
- fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
+ fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))
val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
fun minimize_facts _ time min_facts [] = (time, min_facts)
@@ -43,7 +43,7 @@
val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
in
- set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs
+ set_preplay_outcome l meth (Played time); mk_step_lfs_gfs min_lfs min_gfs
end
| _ => step (* don't touch steps that time out or fail *))
@@ -62,7 +62,7 @@
fold_rev do_step steps (refed, [concl])
end
and do_step step (refed, accu) =
- (case label_of_step step of
+ (case label_of_isar_step step of
NONE => (refed, step :: accu)
| SOME l =>
if Ord_List.member label_ord refed l then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 19:32:13 2014 +0100
@@ -8,6 +8,7 @@
signature SLEDGEHAMMER_ISAR_PREPLAY =
sig
type play_outcome = Sledgehammer_Reconstructor.play_outcome
+ type proof_method = Sledgehammer_Isar_Proof.proof_method
type isar_step = Sledgehammer_Isar_Proof.isar_step
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type label = Sledgehammer_Isar_Proof.label
@@ -15,8 +16,8 @@
val trace : bool Config.T
type isar_preplay_data =
- {get_preplay_outcome: label -> play_outcome,
- set_preplay_outcome: label -> play_outcome -> unit,
+ {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+ set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
@@ -101,12 +102,12 @@
| Force_Method => Clasimp.force_tac ctxt
| Arith_Method => Arith_Data.arith_tac ctxt
| Blast_Method => blast_tac ctxt
+ | Algebra_Method => Groebner.algebra_tac [] [] ctxt
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
-fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime
- | preplay_raw debug type_enc lam_trans ctxt timeout
- (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) =
+fun preplay_raw debug type_enc lam_trans ctxt timeout meth
+ (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
let
val goal =
(case xs of
@@ -144,12 +145,9 @@
play_outcome)
end
-
-(*** proof preplay interface ***)
-
type isar_preplay_data =
- {get_preplay_outcome: label -> play_outcome,
- set_preplay_outcome: label -> play_outcome -> unit,
+ {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+ set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
@@ -188,16 +186,16 @@
fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
if not do_preplay then
(* the "dont_preplay" option pretends that everything works just fine *)
- {get_preplay_outcome = K (Played Time.zeroTime),
- set_preplay_outcome = K (K ()),
+ {preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
+ set_preplay_outcome = K (K (K ())),
preplay_quietly = K (K (Played Time.zeroTime)),
overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
else
let
val ctxt = enrich_context_with_local_facts proof ctxt
- fun preplay quietly timeout step =
- preplay_raw debug type_enc lam_trans ctxt timeout step
+ fun preplay quietly timeout meth step =
+ preplay_raw debug type_enc lam_trans ctxt timeout meth step
handle exn =>
if Exn.is_interrupt exn then
reraise exn
@@ -209,39 +207,41 @@
Play_Failed)
(* preplay steps treating exceptions like timeouts *)
- fun preplay_quietly timeout = preplay true timeout
+ fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
+ preplay true timeout meth step
+ | preplay_quietly _ _ = Played Time.zeroTime
+
+ fun add_step_to_tab (step as Prove (_, _, l, _, _, (_, methss))) =
+ Canonical_Label_Tab.update_new
+ (l, maps (map (fn meth =>
+ (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
+ | add_step_to_tab _ = I
val preplay_tab =
- let
- fun add_step_to_tab step tab =
- (case label_of_step step of
- NONE => tab
- | SOME l =>
- Canonical_Label_Tab.update_new
- (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
- handle Canonical_Label_Tab.DUP _ =>
- raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
- in
- Canonical_Label_Tab.empty
- |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
- |> Unsynchronized.ref
- end
+ Canonical_Label_Tab.empty
+ |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
+ |> Unsynchronized.ref
- fun get_preplay_outcome l =
- Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
- handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
+ fun preplay_outcome l meth =
+ (case Canonical_Label_Tab.lookup (!preplay_tab) l of
+ SOME meths_outcomes =>
+ (case AList.lookup (op =) meths_outcomes meth of
+ SOME outcome => outcome
+ | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
+ | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
- fun set_preplay_outcome l result =
- preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab)
+ fun set_preplay_outcome l meth result =
+ preplay_tab := Canonical_Label_Tab.map_entry l
+ (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
- val result_of_step =
- try (label_of_step #> the #> get_preplay_outcome)
- #> the_default (Played Time.zeroTime)
+ fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
+ Lazy.force (preplay_outcome l meth)
+ | result_of_step _ = Played Time.zeroTime
fun overall_preplay_outcome (Proof (_, _, steps)) =
fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
in
- {get_preplay_outcome = get_preplay_outcome,
+ {preplay_outcome = preplay_outcome,
set_preplay_outcome = set_preplay_outcome,
preplay_quietly = preplay_quietly,
overall_preplay_outcome = overall_preplay_outcome}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 19:32:13 2014 +0100
@@ -13,15 +13,16 @@
datatype isar_qualifier = Show | Then
+ datatype proof_method =
+ Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+ Arith_Method | Blast_Method | Meson_Method | Algebra_Method
+
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method list list)
- and proof_method =
- Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
- Arith_Method | Blast_Method | Meson_Method
val no_label : label
val no_facts : facts
@@ -29,10 +30,12 @@
val label_ord : label * label -> order
val string_of_label : label -> string
+ val string_of_proof_method : proof_method -> string
+
val steps_of_proof : isar_proof -> isar_step list
- val label_of_step : isar_step -> label option
- val byline_of_step : isar_step -> (facts * proof_method list list) option
+ val label_of_isar_step : isar_step -> label option
+ val byline_of_isar_step : isar_step -> (facts * proof_method list list) option
val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
@@ -41,9 +44,14 @@
structure Canonical_Label_Tab : TABLE
val canonical_label_ord : (label * label) -> order
- val relabel_isar_proof_canonically : isar_proof -> isar_proof
- val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
+ val chain_isar_proof : isar_proof -> isar_proof
+ val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
+ val relabel_isar_proof_canonically : isar_proof -> isar_proof
+ val relabel_isar_proof_finally : isar_proof -> isar_proof
+
+ val string_of_isar_proof : Proof.context -> string -> string -> int -> int ->
+ (label -> proof_method list list -> string) -> isar_proof -> string
end;
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
@@ -62,15 +70,16 @@
datatype isar_qualifier = Show | Then
+datatype proof_method =
+ Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+ Arith_Method | Blast_Method | Meson_Method | Algebra_Method
+
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method list list)
-and proof_method =
- Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
- Arith_Method | Blast_Method | Meson_Method
val no_label = ("", ~1)
val no_facts = ([],[])
@@ -79,19 +88,32 @@
fun string_of_label (s, num) = s ^ string_of_int num
+fun string_of_proof_method meth =
+ (case meth of
+ Metis_Method => "metis"
+ | 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"
+ | Algebra_Method => "algebra")
+
fun steps_of_proof (Proof (_, _, steps)) = steps
-fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
- | label_of_step _ = NONE
+fun label_of_isar_step (Prove (_, _, l, _, _, _)) = SOME l
+ | label_of_isar_step _ = NONE
-fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
- | subproofs_of_step _ = NONE
+fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
+ | subproofs_of_isar_step _ = NONE
-fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
- | byline_of_step _ = NONE
+fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = SOME byline
+ | byline_of_isar_step _ = NONE
fun fold_isar_step f step =
- fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) #> f step
+ fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
and fold_isar_steps f = fold (fold_isar_step f)
fun map_isar_steps f =
@@ -111,6 +133,38 @@
type key = label
val ord = canonical_label_ord)
+fun chain_qs_lfs NONE lfs = ([], lfs)
+ | chain_qs_lfs (SOME l0) lfs =
+ if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
+fun chain_isar_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
+ let val (qs', lfs) = chain_qs_lfs lbl lfs in
+ Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, ((lfs, gfs), methss))
+ end
+ | chain_isar_step _ step = step
+and chain_isar_steps _ [] = []
+ | chain_isar_steps (prev as SOME _) (i :: is) =
+ chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
+ | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is
+and chain_isar_proof (Proof (fix, assms, steps)) =
+ Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
+
+fun kill_useless_labels_in_isar_proof proof =
+ let
+ val used_ls =
+ fold_isar_steps (byline_of_isar_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
+ (steps_of_proof proof) []
+
+ fun kill_label l = if member (op =) used_ls l then l else no_label
+
+ fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
+ Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
+ | kill_step step = step
+ and kill_proof (Proof (fix, assms, steps)) =
+ Proof (fix, map (apfst kill_label) assms, map kill_step steps)
+ in
+ kill_proof proof
+ end
+
fun relabel_isar_proof_canonically proof =
let
fun next_label l (next, subst) =
@@ -146,9 +200,51 @@
fst (do_proof proof (0, []))
end
+val assume_prefix = "a"
+val have_prefix = "f"
+
+val relabel_isar_proof_finally =
+ let
+ fun fresh_label depth prefix (accum as (l, subst, next)) =
+ if l = no_label then
+ accum
+ else
+ let val l' = (replicate_string (depth + 1) prefix, next) in
+ (l', (l, l') :: subst, next + 1)
+ end
+
+ fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
+
+ fun relabel_assm depth (l, t) (subst, next) =
+ let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
+ ((l, t), (subst, next))
+ end
+
+ fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
+
+ fun relabel_steps _ _ _ [] = []
+ | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
+ let
+ val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
+ val sub = relabel_proofs subst depth sub
+ val by = apfst (relabel_facts subst) by
+ in
+ Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
+ end
+ | relabel_steps subst depth next (step :: steps) =
+ step :: relabel_steps subst depth next steps
+ and relabel_proof subst depth (Proof (fix, assms, steps)) =
+ let val (assms, subst) = relabel_assms subst depth assms in
+ Proof (fix, assms, relabel_steps subst depth 1 steps)
+ end
+ and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
+ in
+ relabel_proof [] 0
+ end
+
val indent_size = 2
-fun string_of_isar_proof ctxt type_enc lam_trans i n proof =
+fun string_of_isar_proof ctxt type_enc lam_trans i n comment_of proof =
let
(* Make sure only type constraints inserted by the type annotation code are printed. *)
val ctxt =
@@ -160,7 +256,7 @@
val register_fixes = map Free #> fold Variable.auto_fixes
- fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
+ fun add_str s' = apfst (suffix s')
fun of_indent ind = replicate_string (ind * indent_size) " "
fun of_moreover ind = of_indent ind ^ "moreover\n"
@@ -188,18 +284,6 @@
|> 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))
@@ -213,15 +297,7 @@
fun of_method ls ss Metis_Method =
using_facts ls [] ^ by_facts (metis_call type_enc lam_trans) [] ss
| of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "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
+ | of_method ls ss meth = using_facts ls ss ^ "by " ^ string_of_proof_method meth
fun of_free (s, T) =
maybe_quote s ^ " :: " ^
@@ -232,22 +308,17 @@
fun add_fix _ [] = I
| add_fix ind xs =
- add_suffix (of_indent ind ^ "fix ")
+ add_str (of_indent ind ^ "fix ")
#> add_frees xs
- #> add_suffix "\n"
+ #> add_str "\n"
fun add_assm ind (l, t) =
- add_suffix (of_indent ind ^ "assume " ^ of_label l)
+ add_str (of_indent ind ^ "assume " ^ of_label l)
#> add_term t
- #> add_suffix "\n"
+ #> add_str "\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
@@ -266,20 +337,22 @@
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_str (of_indent ind ^ "let ")
+ #> add_term t1 #> add_str " = " #> add_term t2
+ #> add_str "\n"
+ | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), methss as (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
+ [] => add_str (of_have qs (length subproofs) ^ " ")
+ | _ =>
+ add_str (of_obtain qs (length subproofs) ^ " ") #> add_frees xs #> add_str " where ")
+ #> add_str (of_label l)
+ #> add_term t
+ #> add_str (" " ^
+ of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
+ (case comment_of l methss of
+ "" => ""
+ | comment => " (* " ^ comment ^ " *)") ^ "\n")
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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 19:32:13 2014 +0100
@@ -30,11 +30,11 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
- (step as Prove (_, _, l, _, _, _)) =
+ ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
+ (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
let
val timeout =
- (case get_preplay_outcome l of
+ (case Lazy.force (preplay_outcome l meth) of
Played time => Time.+ (time, slack)
| _ => preplay_timeout)
@@ -44,7 +44,8 @@
| _ => NONE)
in
(case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step', result) => (set_preplay_outcome l result; step')
+ SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
+ (set_preplay_outcome l meth' result; step')
| NONE => step)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 31 19:32:13 2014 +0100
@@ -8,6 +8,7 @@
sig
val sledgehammerN : string
val log2 : real -> real
+ val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
val app_hd : ('a -> 'a) -> 'a list -> 'a list
val n_fold_cartesian_product : 'a list list -> 'a list list
val plural_s : int -> string
@@ -38,6 +39,8 @@
val log10_2 = Math.log10 2.0
fun log2 n = Math.log10 n / log10_2
+fun map3 xs = Ctr_Sugar_Util.map3 xs
+
fun app_hd f (x :: xs) = f x :: xs
fun cartesian_product [] _ = []