avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
authorsmolkas
Mon May 06 11:03:08 2013 +0200 (2013-05-06 ago)
changeset 5187771052c42edf2
parent 51876 724c67f59929
child 51878 f11039b31bae
avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon May 06 11:03:08 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon May 06 11:03:08 2013 +0200
     1.3 @@ -134,8 +134,8 @@
     1.4          if p <> cp then
     1.5            (env, cp + 1, ps, annots)
     1.6          else
     1.7 -          let val (_, (env', T')) = get_annot env T in
     1.8 -            (env', cp + 1, ps', (p, T') :: annots)
     1.9 +          let val (annot_necessary, (env', T')) = get_annot env T in
    1.10 +            (env', cp + 1, ps', annots |> annot_necessary ? cons (p, T'))
    1.11            end
    1.12        | post1 _ _ accum = accum
    1.13      val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon May 06 11:03:08 2013 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon May 06 11:03:08 2013 +0200
     2.3 @@ -170,6 +170,7 @@
     2.4          if Inttab.is_empty cand_tab
     2.5            orelse n_metis' <= target_n_metis
     2.6            orelse (on_top_level andalso n'<3)
     2.7 +          orelse metis_fail()
     2.8          then
     2.9            (Vector.foldr
    2.10               (fn (NONE, steps) => steps | (SOME s, steps) => s :: steps)
    2.11 @@ -187,12 +188,14 @@
    2.12                merge_steps metis_time step_vect refed_by cand_tab n' n_metis'
    2.13              | (s, metis_time) =>
    2.14              let
    2.15 -              val refs = refs s1
    2.16 +              val refs_s1 = refs s1
    2.17                val refed_by = refed_by |> fold
    2.18 -                (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
    2.19 +                (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j))
    2.20 +                refs_s1
    2.21 +              val shared_refs = Ord_List.inter int_ord refs_s1 (refs s2)
    2.22                val new_candidates =
    2.23                  fold (add_if_cand step_vect)
    2.24 -                  (map (fn i => (i, get i refed_by)) refs) []
    2.25 +                  (map (fn i => (i, get i refed_by)) shared_refs) []
    2.26                val cand_tab = add_list cand_tab new_candidates
    2.27                val step_vect = step_vect |> replace NONE i |> replace s j
    2.28              in