--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 11:58:38 2014 +0100
@@ -169,7 +169,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
@@ -218,7 +218,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
@@ -229,9 +229,6 @@
val rule = rule_of_clause_id id
val skolem = is_skolemize_rule rule
- fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
- fun steps_of_rest l step = isar_steps outer (SOME l) (step :: accum) infs
-
val deps = fold add_fact_of_dependencies gamma ([], [])
val meths =
(if skolem then skolem_methods
@@ -239,21 +236,23 @@
else if is_datatype_rule rule then datatype_methods
else metislike_methods)
|> massage_meths
- val by = (deps, 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
(case gamma of
[g] =>
if skolem andalso is_clause_tainted g then
let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
- isar_steps outer (SOME l) [prove [subproof] (([], []), meths)] infs
+ isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
end
else
- steps_of_rest l (prove [] by)
- | _ => steps_of_rest l (prove [] by))
+ steps_of_rest (prove [] deps)
+ | _ => steps_of_rest (prove [] deps))
else
- steps_of_rest l
- (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
+ 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) =
let
@@ -265,7 +264,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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 11:58:38 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,15 +55,15 @@
| 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, by))
- (steps, updates as Prove (qs', xs', l', t', subproofs', by') :: 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, by') :: steps, updates)
- else (Prove (qs, xs, l, t, subproofs, by) :: steps, updates)
+ 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
and update_subproofs [] updates = ([], updates)
| update_subproofs steps [] = (steps, [])
@@ -80,8 +80,8 @@
| _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
end
-fun try_merge (Prove (_, [], l1, _, [], ((lfs1, gfs1), meths1)))
- (Prove (qs2, fix, l2, t, subproofs, ((lfs2, gfs2), meths2))) =
+fun try_merge (Prove (_, [], l1, _, [], (lfs1, gfs1), meths1))
+ (Prove (qs2, fix, l2, t, subproofs, (lfs2, gfs2), meths2)) =
(case inter (op =) meths1 meths2 of
[] => NONE
| meths =>
@@ -89,7 +89,7 @@
val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
val gfs = union (op =) gfs1 gfs2
in
- SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths)))
+ SOME (Prove (qs2, fix, l2, t, subproofs, (lfs, gfs), meths))
end)
| try_merge _ _ = NONE
@@ -118,7 +118,7 @@
val (get_successors, replace_successor) =
let
fun add_refs (Let _) = I
- | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
+ | add_refs (Prove (_, _, v, _, _, (lfs, _), _)) =
fold (fn key => Canonical_Label_Tab.cons_list (key, v)) lfs
val tab =
@@ -144,7 +144,7 @@
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)
in
set_preplay_outcomes_of_isar_step ctxt time preplay_data step [(meth, Played time)];
step
@@ -154,7 +154,7 @@
(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
+ 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'
@@ -163,8 +163,8 @@
val subs'' = subs @ nontriv_subs
val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
val gfs'' = union (op =) gfs' gfs
- val by = ((lfs'', gfs''), meths(*FIXME*))
- val step'' = Prove (qs, fix, l, t, subs'', by)
+ val meths'' as _ :: _ = inter (op =) meths' meths
+ val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'')
(* check if the modified step can be preplayed fast enough *)
val timeout = slackify_merge_timeout (Time.+ (time, time'))
@@ -179,7 +179,7 @@
| _ => 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))) =
+ | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)) =
if subproofs = [] then
step
else
@@ -208,7 +208,7 @@
val candidates =
let
fun add_cand (_, Let _) = I
- | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
+ | add_cand (i, Prove (_, _, l, t, _, _, _)) = cons (i, l, size_of_term t)
in
(steps
|> split_last |> fst (* keep last step *)
@@ -217,7 +217,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
@@ -280,9 +280,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, by)) =
+ | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths)) =
(* compress subproofs *)
- Prove (qs, xs, l, t, map compress_proof subproofs, by)
+ Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths)
(* eliminate trivial subproofs *)
|> compress_further () ? elim_subproofs
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 11:58:38 2014 +0100
@@ -25,19 +25,18 @@
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
-fun keep_fastest_method_of_isar_step preplay_data
- (Prove (qs, xs, l, t, subproofs, (facts, _))) =
- Prove (qs, xs, l, t, subproofs, (facts, [fastest_method_of_isar_step preplay_data l]))
+fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, _)) =
+ Prove (qs, xs, l, t, subproofs, facts, [fastest_method_of_isar_step preplay_data l])
| 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 :: _)) =
(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)
fun minimize_facts _ time min_facts [] = (time, min_facts)
| minimize_facts mk_step time min_facts (f :: facts) =
@@ -76,16 +75,15 @@
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)) =
let
val (used, subproofs) =
map process_proof subproofs
|> split_list
|>> Ord_List.unions label_ord
|>> fold (Ord_List.insert label_ord) lfs
- val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
in
- (used, step)
+ (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths))
end
in
snd o process_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 11:58:38 2014 +0100
@@ -53,7 +53,7 @@
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, _)) =
+ | enrich_with_step (Prove (_, _, l, t, subproofs, _, _)) =
enrich_with_fact l t #> fold enrich_with_proof subproofs
in
enrich_with_proof proof ctxt
@@ -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
@@ -122,8 +122,7 @@
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth
- (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
+fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
let
val goal =
(case xs of
@@ -186,7 +185,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)
@@ -229,7 +228,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 (the_single meths))
| forced_outcome_of_step _ _ = Played Time.zeroTime
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 11:58:38 2014 +0100
@@ -29,8 +29,8 @@
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)
+ Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
+ * facts * proof_method list
val no_label : label
@@ -94,8 +94,8 @@
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)
+ Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
+ * facts * proof_method list
val no_label = ("", ~1)
@@ -120,16 +120,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 (_, _, _, _, subproofs, _)) = SOME subproofs
+fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _, _)) = SOME subproofs
| subproofs_of_isar_step _ = NONE
-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 =
@@ -140,8 +140,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, subproofs, by)) =
- f (Prove (qs, xs, l, t, map map_proof subproofs, by))
+ | map_step (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+ f (Prove (qs, xs, l, t, map map_proof subproofs, facts, meths))
in map_proof end
val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
@@ -156,9 +156,9 @@
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), meths))) =
+fun chain_isar_step lbl (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) =
let val (qs', lfs) = chain_qs_lfs lbl lfs in
- Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, ((lfs, gfs), meths))
+ Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, (lfs, gfs), meths)
end
| chain_isar_step _ step = step
and chain_isar_steps _ [] = []
@@ -175,8 +175,8 @@
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)
+ fun kill_step (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+ Prove (qs, xs, kill_label l, t, map kill_proof subproofs, facts, meths)
| kill_step step = step
and kill_proof (Proof (fix, assms, steps)) =
Proof (fix, map (apfst kill_label) assms, map kill_step steps)
@@ -189,14 +189,13 @@
fun next_label l (next, subst) =
let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
- fun relabel_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by
- handle Option.Option =>
- raise Fail "Sledgehammer_Isar_Proof: relabel_isar_proof_canonically"
+ fun relabel_facts (lfs, gfs) (_, subst) =
+ (map (AList.lookup (op =) subst #> the) lfs, gfs)
+ handle Option.Option =>
+ raise Fail "Sledgehammer_Isar_Proof: relabel_isar_proof_canonically"
fun relabel_assm (l, t) state =
- let
- val (l, state) = next_label l state
- in ((l, t), state) end
+ next_label l state |> (fn (l, state) => ((l, t), state))
fun relabel_proof (Proof (fix, assms, steps)) state =
let
@@ -206,15 +205,15 @@
(Proof (fix, assms, steps), state)
end
- and relabel_step (step as Let _) state = (step, state)
- | relabel_step (Prove (qs, fix, l, t, subproofs, by)) state=
+ and relabel_step (Prove (qs, fix, l, t, subproofs, facts, meths)) state =
let
- val by = relabel_byline by state
+ val facts = relabel_facts facts state
val (subproofs, state) = fold_map relabel_proof subproofs state
val (l, state) = next_label l state
in
- (Prove (qs, fix, l, t, subproofs, by), state)
+ (Prove (qs, fix, l, t, subproofs, facts, meths), state)
end
+ | relabel_step step state = (step, state)
in
fst (relabel_proof proof (0, []))
end
@@ -242,13 +241,13 @@
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) =
+ | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, facts, meths) :: 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
+ val facts = relabel_facts subst facts
in
- Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
+ Prove (qs, xs, l, t, sub, facts, meths) :: relabel_steps subst depth next steps
end
| relabel_steps subst depth next (step :: steps) =
step :: relabel_steps subst depth next steps
@@ -367,7 +366,7 @@
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), meths as meth :: _))) =
+ | add_step ind (Prove (qs, xs, l, t, subproofs, (ls, ss), meths as meth :: _)) =
add_step_pre ind qs subproofs
#> (case xs of
[] => add_str (of_have qs (length subproofs) ^ " ")
@@ -387,7 +386,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 ^