--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:32:02 2014 +0100
@@ -174,7 +174,7 @@
else ([], rewrite_methods))
||> massage_meths
in
- Prove ([], skos, l, t, [], ([], []), meths)
+ Prove ([], skos, l, t, [], ([], []), meths, "")
end)
val bot = atp_proof |> List.last |> #1
@@ -223,7 +223,7 @@
accum
|> (if tainted = [] then
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- (the_list predecessor, []), massage_meths metislike_methods))
+ (the_list predecessor, []), massage_meths metislike_methods, ""))
else
I)
|> rev
@@ -242,7 +242,7 @@
else metislike_methods)
|> massage_meths
- fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths)
+ fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "")
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
in
if is_clause_tainted c then
@@ -256,7 +256,7 @@
steps_of_rest (prove [] deps)
| _ => steps_of_rest (prove [] deps))
else
- steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths)
+ steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths, "")
else prove [] deps)
end
| isar_steps outer predecessor accum (Cases cases :: infs) =
@@ -269,7 +269,7 @@
val step =
Prove (maybe_show outer c [], [], l, t,
map isar_case (filter_out (null o snd) cases),
- (the_list predecessor, []), massage_meths metislike_methods)
+ (the_list predecessor, []), massage_meths metislike_methods, "")
in
isar_steps outer (SOME l) (step :: accum) infs
end
@@ -299,7 +299,6 @@
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_of_isar_step_for_method (!preplay_data) l meth)
@@ -307,11 +306,17 @@
fun trace_isar_proof label proof =
if trace then
- tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
- "\n")
+ tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
+ string_of_isar_proof (comment_isar_proof comment_of proof) ^ "\n")
else
()
+ fun comment_of l (meth :: _) =
+ (case (verbose,
+ Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
+ (false, Played _) => ""
+ | (_, outcome) => string_of_play_outcome outcome)
+
val (play_outcome, isar_proof) =
canonical_isar_proof
|> tap (trace_isar_proof "Original")
@@ -322,11 +327,12 @@
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
|> tap (trace_isar_proof "Minimized")
|> `(preplay_outcome_of_isar_proof (!preplay_data))
+ ||> comment_isar_proof comment_of
||> chain_isar_proof
||> kill_useless_labels_in_isar_proof
||> relabel_isar_proof_nicely
in
- (case string_of_isar_proof (K (K "")) isar_proof of
+ (case string_of_isar_proof 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 Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 19:32:02 2014 +0100
@@ -32,7 +32,7 @@
| collect_steps [] accum = accum
| collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)
and collect_step (Let _) x = x
- | collect_step (step as Prove (_, _, l, _, subproofs, _, _)) x =
+ | collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x =
(case collect_subproofs subproofs x of
([], accu) => ([], accu)
| accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
@@ -55,16 +55,16 @@
| update_steps (step :: steps) updates = update_step step (update_steps steps updates)
and update_step step (steps, []) = (step :: steps, [])
| update_step (step as Let _) (steps, updates) = (step :: steps, updates)
- | update_step (Prove (qs, xs, l, t, subproofs, facts, meths))
- (steps, updates as Prove (qs', xs', l', t', subproofs', facts', meths') :: updates') =
- let
- val (subproofs, updates) =
- if l = l' then update_subproofs subproofs' updates'
- else update_subproofs subproofs updates
- in
- if l = l' then (Prove (qs', xs', l', t', subproofs, facts', meths') :: steps, updates)
- else (Prove (qs, xs, l, t, subproofs, facts, meths) :: steps, updates)
- end
+ | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment))
+ (steps,
+ updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') =
+ (if l = l' then
+ update_subproofs subproofs' updates'
+ |>> (fn subproofs' => Prove (qs', xs', l', t', subproofs', facts', meths', comment'))
+ else
+ update_subproofs subproofs updates
+ |>> (fn subproofs => Prove (qs, xs, l, t, subproofs, facts, meths, comment)))
+ |>> (fn step => step :: steps)
and update_subproofs [] updates = ([], updates)
| update_subproofs steps [] = (steps, [])
| update_subproofs (proof :: subproofs) updates =
@@ -91,8 +91,8 @@
inter (op =) (filter (is_method_hopeful l1) meths1) (filter (is_method_hopeful l2) meths2)
end
-fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1))
- (Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2)) =
+fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
+ (Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
(case merge_methods preplay_data (l1, meths1) (l2, meths2) of
[] => NONE
| meths =>
@@ -100,7 +100,8 @@
val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
val gfs = union (op =) gfs1 gfs2
in
- SOME (Prove (qs2, fix, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths))
+ SOME (Prove (qs2, fix, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths,
+ comment1 ^ comment2))
end)
| try_merge _ _ _ = NONE
@@ -128,9 +129,9 @@
val (get_successors, replace_successor) =
let
- fun add_refs (Let _) = I
- | add_refs (Prove (_, _, v, _, _, (lfs, _), _)) =
- fold (fn key => Canonical_Label_Tab.cons_list (key, v)) lfs
+ fun add_refs (Prove (_, _, l, _, _, (lfs, _), _, _)) =
+ fold (fn key => Canonical_Label_Tab.cons_list (key, l)) lfs
+ | add_refs _ = I
val tab =
Canonical_Label_Tab.empty
@@ -151,11 +152,11 @@
end
(* elimination of trivial, one-step subproofs *)
- fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
+ fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) comment subs nontriv_subs =
if null subs orelse not (compress_further ()) then
let
val subproofs = List.revAppend (nontriv_subs, subs)
- val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)
+ val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)
in
set_preplay_outcomes_of_isar_step ctxt time preplay_data step [(meth, Played time)];
step
@@ -165,7 +166,7 @@
(sub as Proof (_, assms, sub_steps)) :: subs =>
(let
(* trivial subproofs have exactly one "Prove" step *)
- val [Prove (_, [], l', _, [], (lfs', gfs'), meths')] = sub_steps
+ val [Prove (_, [], l', _, [], (lfs', gfs'), meths', _)] = sub_steps
(* only touch proofs that can be preplayed sucessfully *)
val Played time' = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l'
@@ -175,7 +176,7 @@
val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
val gfs'' = union (op =) gfs' gfs
val meths'' as _ :: _ = merge_methods (!preplay_data) (l', meths') (l, meths)
- val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'')
+ val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'', comment)
(* check if the modified step can be preplayed fast enough *)
val timeout = slackify_merge_timeout (Time.+ (time, time'))
@@ -183,20 +184,20 @@
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
- elim_one_subproof time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
+ elim_one_subproof time'' qs fix l t lfs'' gfs'' meths comment subs nontriv_subs
end
handle Bind =>
- elim_one_subproof time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
+ elim_one_subproof time qs fix l t lfs gfs meths comment subs (sub :: nontriv_subs))
| _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
- fun elim_subproofs (step as Let _) = step
- | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)) =
+ fun elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)) =
if subproofs = [] then
step
else
(case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of
- Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
+ Played time => elim_one_subproof time qs fix l t lfs gfs meths comment subproofs []
| _ => step)
+ | elim_subproofs step = step
fun compress_top_level steps =
let
@@ -218,8 +219,8 @@
val candidates =
let
- fun add_cand (_, Let _) = I
- | add_cand (i, Prove (_, _, l, t, _, _, _)) = cons (i, l, size_of_term t)
+ fun add_cand (i, Prove (_, _, l, t, _, _, _, _)) = cons (i, l, size_of_term t)
+ | add_cand _ = I
in
(steps
|> split_last |> fst (* keep last step *)
@@ -228,7 +229,7 @@
fun try_eliminate (i, l, _) labels steps =
let
- val ((cand as Prove (_, _, _, _, _, (lfs, _), _)) :: steps') = drop i steps
+ val ((cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps') = drop i steps
val succs = collect_successors steps' labels
@@ -292,9 +293,9 @@
steps |> map (fn step => step |> compress_further () ? compress_sub_levels)
|> compress_further () ? compress_top_level
and compress_sub_levels (step as Let _) = step
- | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+ | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
(* compress subproofs *)
- Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths)
+ Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment)
(* eliminate trivial subproofs *)
|> compress_further () ? elim_subproofs
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 19:32:02 2014 +0100
@@ -25,19 +25,21 @@
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
-fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+fun keep_fastest_method_of_isar_step preplay_data
+ (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
Prove (qs, xs, l, t, subproofs, facts,
- meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @)
+ meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @,
+ comment)
| keep_fastest_method_of_isar_step _ step = step
val slack = seconds 0.1
fun minimize_isar_step_dependencies ctxt preplay_data
- (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _)) =
+ (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
Played time =>
let
- fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)
+ fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
fun minimize_facts _ time min_facts [] = (time, min_facts)
| minimize_facts mk_step time min_facts (f :: facts) =
@@ -76,7 +78,7 @@
else
(used, accu))
and process_used_step step = step |> postproc_step |> process_used_step_subproofs
- and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) =
+ and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) =
let
val (used, subproofs) =
map process_proof subproofs
@@ -84,7 +86,7 @@
|>> Ord_List.unions label_ord
|>> fold (Ord_List.insert label_ord) lfs
in
- (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths))
+ (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment))
end
in
snd o process_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 19:32:02 2014 +0100
@@ -52,9 +52,9 @@
fun enrich_with_proof (Proof (_, assms, isar_steps)) =
enrich_with_assms assms #> fold enrich_with_step isar_steps
- and enrich_with_step (Let _) = I
- | enrich_with_step (Prove (_, _, l, t, subproofs, _, _)) =
+ and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) =
enrich_with_fact l t #> fold enrich_with_proof subproofs
+ | enrich_with_step _ = I
in
enrich_with_proof proof ctxt
end
@@ -88,7 +88,7 @@
val concl =
(case try List.last steps of
- SOME (Prove (_, [], _, t, _, _, _)) => t
+ SOME (Prove (_, [], _, t, _, _, _, _)) => t
| _ => raise Fail "preplay error: malformed subproof")
val var_idx = maxidx_of_term concl + 1
@@ -100,8 +100,8 @@
|> Skip_Proof.make_thm thy
end
-(* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
+(* may throw exceptions *)
+fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
let
val goal =
(case xs of
@@ -122,18 +122,18 @@
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
end)
- val facts =
- resolve_fact_names ctxt fact_names
+ val assmsp =
+ resolve_fact_names ctxt facts
|>> append (map (thm_of_proof ctxt) subproofs)
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
- HEADGOAL (tac_of_proof_method ctxt facts meth))
+ HEADGOAL (tac_of_proof_method ctxt assmsp meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
val play_outcome = take_time timeout prove ()
in
- (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
+ (if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
play_outcome)
end
@@ -164,7 +164,7 @@
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
- (step as Prove (_, _, l, _, _, _, meths)) meths_outcomes0 =
+ (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
let
fun lazy_preplay meth =
Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
@@ -207,7 +207,7 @@
#> get_best_method_outcome Lazy.force
#> fst
-fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths)) =
+fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) =
Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths))
| forced_outcome_of_step _ _ = Played Time.zeroTime
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 19:32:02 2014 +0100
@@ -20,7 +20,7 @@
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
- * facts * proof_method list
+ * facts * proof_method list * string
val no_label : label
@@ -41,13 +41,13 @@
val canonical_label_ord : (label * label) -> order
+ val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
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_nicely : isar_proof -> isar_proof
- val string_of_isar_proof : Proof.context -> int -> int ->
- (label -> proof_method list -> string) -> isar_proof -> string
+ val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
end;
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
@@ -71,7 +71,7 @@
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
- * facts * proof_method list
+ * facts * proof_method list * string
val no_label = ("", ~1)
@@ -81,16 +81,16 @@
fun steps_of_isar_proof (Proof (_, _, steps)) = steps
-fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l
+fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
| label_of_isar_step _ = NONE
-fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _)) = subs
+fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs
| subproofs_of_isar_step _ = []
-fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _)) = facts
+fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts
| facts_of_isar_step _ = ([], [])
-fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths)) = meths
+fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths
| proof_methods_of_isar_step _ = []
fun fold_isar_step f step =
@@ -101,8 +101,8 @@
let
fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
and map_step (step as Let _) = f step
- | map_step (Prove (qs, xs, l, t, subs, facts, meths)) =
- f (Prove (qs, xs, l, t, map map_proof subs, facts, meths))
+ | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
+ f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
in map_proof end
val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
@@ -114,12 +114,17 @@
type key = label
val ord = canonical_label_ord)
+fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) =
+ Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths)
+ | comment_isar_step _ step = step
+fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of)
+
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, subs, (lfs, gfs), meths)) =
+fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
let val (qs', lfs) = chain_qs_lfs lbl lfs in
- Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths)
+ Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
end
| chain_isar_step _ step = step
and chain_isar_steps _ [] = []
@@ -136,8 +141,8 @@
fun kill_label l = if member (op =) used_ls l then l else no_label
- fun kill_step (Prove (qs, xs, l, t, subs, facts, meths)) =
- Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths)
+ fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
+ Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment)
| kill_step step = step
and kill_proof (Proof (fix, assms, steps)) =
Proof (fix, map (apfst kill_label) assms, map kill_step steps)
@@ -150,14 +155,15 @@
fun next_label l (next, subst) =
let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
- fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) =
+ fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment))
+ (accum as (_, subst)) =
let
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
val ((subs', l'), accum') = accum
|> fold_map relabel_proof subs
||>> next_label l
in
- (Prove (qs, fix, l', t, subs', (lfs', gfs), meths), accum')
+ (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum')
end
| relabel_step step accum = (step, accum)
and relabel_proof (Proof (fix, assms, steps)) =
@@ -181,13 +187,14 @@
(l', (next + 1, (l, l') :: subst))
end
- fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) =
+ fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment))
+ (accum as (_, subst)) =
let
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
val (l', accum' as (next', subst')) = next_label depth have_prefix l accum
val subs' = map (relabel_proof subst' (depth + 1)) subs
in
- (Prove (qs, xs, l', t, subs', (lfs', gfs), meths), accum')
+ (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
end
| relabel_step _ step accum = (step, accum)
and relabel_proof subst depth (Proof (fix, assms, steps)) =
@@ -201,7 +208,7 @@
val indent_size = 2
-fun string_of_isar_proof ctxt i n comment_of proof =
+fun string_of_isar_proof ctxt i n proof =
let
(* Make sure only type constraints inserted by the type annotation code are printed. *)
val ctxt =
@@ -298,7 +305,7 @@
and add_step ind (Let (t1, t2)) =
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, subs, (ls, ss), meths as meth :: _)) =
+ | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meths as meth :: _, comment)) =
add_step_pre ind qs subs
#> (case xs of
[] => add_str (of_have qs (length subs) ^ " ")
@@ -307,9 +314,7 @@
#> add_term t
#> add_str (" " ^
of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
- (case comment_of l meths of
- "" => ""
- | comment => " (* " ^ comment ^ " *)") ^ "\n")
+ (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
and add_steps ind = fold (add_step ind)
and of_proof ind ctxt (Proof (xs, assms, steps)) =
("", ctxt)
@@ -321,7 +326,7 @@
(* 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 _ :: _)]) => ""
+ | 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 ^