--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Sun Feb 02 20:53:51 2014 +0100
@@ -20,15 +20,14 @@
structure Sledgehammer_Isar_Annotate : SLEDGEHAMMER_ISAR_ANNOTATE =
struct
-(* Util *)
fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
| post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
| post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
| post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
| post_traverse_term_type' f env (Abs (x, T1, b)) s =
- let
- val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
- in f (Abs (x, T1, b')) (T1 --> T2) s' end
+ let val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s in
+ f (Abs (x, T1, b')) (T1 --> T2) s'
+ end
| post_traverse_term_type' f env (u $ v) s =
let
val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
@@ -49,25 +48,13 @@
end
| _ => f T s
-(** get unique elements of a list **)
-local
- fun unique' b x [] = if b then [x] else []
- | unique' b x (y :: ys) =
- if x = y then unique' false x ys
- else unique' true y ys |> b ? cons x
-in
- fun unique ord xs =
- case sort ord xs of x :: ys => unique' true x ys | [] => []
-end
-
-(** Data structures, orders **)
val indexname_ord = Term_Ord.fast_indexname_ord
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
+
structure Var_Set_Tab = Table(
type key = indexname list
val ord = list_ord indexname_ord)
-(* (1) Generalize types *)
fun generalize_types ctxt t =
let
val erase_types = map_types (fn _ => dummyT)
@@ -78,7 +65,6 @@
t |> erase_types |> infer_types
end
-(* (2) match types *)
fun match_types ctxt t1 t2 =
let
val thy = Proof_Context.theory_of ctxt
@@ -88,17 +74,14 @@
handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Isar_Annotate: match_types"
end
-
-(* (3) handle trivial tfrees *)
fun handle_trivial_tfrees ctxt (t', subst) =
let
- val add_tfree_names =
- snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
+ val add_tfree_names = snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
val trivial_tfree_names =
Vartab.fold add_tfree_names subst []
|> filter_out (Variable.is_declared ctxt)
- |> unique fast_string_ord
+ |> distinct (op =)
val tfree_name_trivial = Ord_List.member fast_string_ord trivial_tfree_names
val trivial_tvar_names =
@@ -128,30 +111,26 @@
(t', subst)
end
-(* (4) Typing-spot table *)
-local
fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z
| key_of_atype _ = I
fun key_of_type T = fold_atyps key_of_atype T []
+
fun update_tab t T (tab, pos) =
- (case key_of_type T of
+ ((case key_of_type T of
[] => tab
| key =>
let val cost = (size_of_typ T, (size_of_term t, pos)) in
- case Var_Set_Tab.lookup tab key of
+ (case Var_Set_Tab.lookup tab key of
NONE => Var_Set_Tab.update_new (key, cost) tab
| SOME old_cost =>
(case cost_ord (cost, old_cost) of
- LESS => Var_Set_Tab.update (key, cost) tab
- | _ => tab)
- end,
+ LESS => Var_Set_Tab.update (key, cost) tab
+ | _ => tab))
+ end),
pos + 1)
-in
-val typing_spot_table =
- post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
-end
-(* (5) Reverse-greedy *)
+val typing_spot_table = post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
+
fun reverse_greedy typing_spot_tab =
let
fun update_count z =
@@ -159,53 +138,53 @@
let val c = Vartab.lookup tab tvar |> the_default 0 in
Vartab.update (tvar, c + z) tab
end)
- fun superfluous tcount =
- forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
+ fun superfluous tcount = forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
else (spot :: spots, tcount)
+
val (typing_spots, tvar_count_tab) =
- Var_Set_Tab.fold
- (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
+ Var_Set_Tab.fold (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
typing_spot_tab ([], Vartab.empty)
|>> sort_distinct (rev_order o cost_ord o pairself snd)
- in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
+ in
+ fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst
+ end
-(* (6) Introduce annotations *)
fun introduce_annotations subst spots t t' =
let
fun subst_atype (T as TVar (idxn, S)) subst =
(Envir.subst_type subst T, Vartab.update (idxn, (S, dummyT)) subst)
| subst_atype T subst = (T, subst)
+
val subst_type = fold_map_atypes subst_atype
+
fun collect_annot _ T (subst, cp, ps as p :: ps', annots) =
if p <> cp then
(subst, cp + 1, ps, annots)
else
let val (T, subst) = subst_type T subst in
- (subst, cp + 1, ps', (p, T)::annots)
+ (subst, cp + 1, ps', (p, T) :: annots)
end
| collect_annot _ _ x = x
- val (_, _, _, annots) =
- post_fold_term_type collect_annot (subst, 0, spots, []) t'
+
+ val (_, _, _, annots) = post_fold_term_type collect_annot (subst, 0, spots, []) t'
+
fun insert_annot t _ (cp, annots as (p, T) :: annots') =
if p <> cp then (t, (cp + 1, annots)) else (Type.constraint T t, (cp + 1, annots'))
| insert_annot t _ x = (t, x)
in
- t |> post_traverse_term_type insert_annot (0, rev annots)
- |> fst
+ t |> post_traverse_term_type insert_annot (0, rev annots) |> fst
end
-(* (7) Annotate *)
fun annotate_types_in_term ctxt t =
let
val t' = generalize_types ctxt t
val subst = match_types ctxt t' t
val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt
- val typing_spots =
- t' |> typing_spot_table
- |> reverse_greedy
- |> sort int_ord
- in introduce_annotations subst typing_spots t t' end
+ val typing_spots = t' |> typing_spot_table |> reverse_greedy |> sort int_ord
+ in
+ introduce_annotations subst typing_spots t t'
+ end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 20:53:51 2014 +0100
@@ -135,8 +135,7 @@
(get_successors, replace_successor)
end
- (** elimination of trivial, one-step subproofs **)
-
+ (* elimination of trivial, one-step subproofs *)
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 meth (Played time);
@@ -249,7 +248,7 @@
decrement_step_count (); (* candidate successfully eliminated *)
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 *)
+ (* removing the step would mess up the indices; replace with dummy step instead *)
steps1 @ dummy_isar_step :: steps2
end
handle Bind => steps
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100
@@ -26,7 +26,8 @@
val slack = seconds 0.1
fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
- | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
+ | minimize_isar_step_dependencies
+ {reset_preplay_outcomes, set_preplay_outcome, 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 =>
@@ -42,8 +43,12 @@
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
+
+ val step' = mk_step_lfs_gfs min_lfs min_gfs
in
- set_preplay_outcome l meth (Played time); mk_step_lfs_gfs min_lfs min_gfs
+ reset_preplay_outcomes step';
+ set_preplay_outcome l meth (Played time);
+ step'
end
| _ => step (* don't touch steps that time out or fail *))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
@@ -16,8 +16,9 @@
val trace : bool Config.T
type isar_preplay_data =
- {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+ {reset_preplay_outcomes: isar_step -> unit,
set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+ preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
@@ -146,8 +147,9 @@
end
type isar_preplay_data =
- {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+ {reset_preplay_outcomes: isar_step -> unit,
set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+ preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
@@ -186,8 +188,9 @@
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 *)
- {preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
+ {reset_preplay_outcomes = K (),
set_preplay_outcome = K (K (K ())),
+ preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
preplay_quietly = K (K (Played Time.zeroTime)),
overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
else
@@ -211,16 +214,17 @@
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 = Unsynchronized.ref Canonical_Label_Tab.empty
- val preplay_tab =
- Canonical_Label_Tab.empty
- |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
- |> Unsynchronized.ref
+ fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, methss))) =
+ preplay_tab := Canonical_Label_Tab.update (l, maps (map (fn meth =>
+ (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
+ (!preplay_tab)
+ | reset_preplay_outcomes _ = ()
+
+ fun set_preplay_outcome l meth result =
+ preplay_tab := Canonical_Label_Tab.map_entry l
+ (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
fun preplay_outcome l meth =
(case Canonical_Label_Tab.lookup (!preplay_tab) l of
@@ -230,9 +234,7 @@
| NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
| NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
- 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 _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
Lazy.force (preplay_outcome l meth)
@@ -241,8 +243,9 @@
fun overall_preplay_outcome (Proof (_, _, steps)) =
fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
in
- {preplay_outcome = preplay_outcome,
+ {reset_preplay_outcomes = reset_preplay_outcomes,
set_preplay_outcome = set_preplay_outcome,
+ preplay_outcome = preplay_outcome,
preplay_quietly = preplay_quietly,
overall_preplay_outcome = overall_preplay_outcome}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100
@@ -43,6 +43,7 @@
result as Played _ => SOME (variant, result)
| _ => NONE)
in
+ (* FIXME: create variant after success *)
(case Par_List.get_some try_variant (variants_of_step step) of
SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
(set_preplay_outcome l meth' result; step')