make sure add: doesn't add duplicates, and works for [no_atp] facts
authorblanchet
Fri Oct 18 00:05:31 2013 +0200 (2013-10-18 ago)
changeset 5414318def1c73c79
parent 54142 5f3c1b445253
child 54144 0fadd32e8d50
make sure add: doesn't add duplicates, and works for [no_atp] facts
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/TPTP/mash_export.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Oct 17 23:41:00 2013 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Oct 18 00:05:31 2013 +0200
     1.3 @@ -128,6 +128,7 @@
     1.4                 Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
     1.5                 hyp_ts concl_t
     1.6             |> filter (is_appropriate_prop o prop_of o snd)
     1.7 +           |> Sledgehammer_Fact.drop_duplicate_facts
     1.8             |> Sledgehammer_MePo.mepo_suggested_facts ctxt params
     1.9                    (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t
    1.10              |> map (fst o fst)
     2.1 --- a/src/HOL/TPTP/mash_export.ML	Thu Oct 17 23:41:00 2013 +0200
     2.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Oct 18 00:05:31 2013 +0200
     2.3 @@ -245,6 +245,7 @@
     2.4                val suggs =
     2.5                  old_facts
     2.6                  |> linearize ? filter_accessible_from th
     2.7 +                |> Sledgehammer_Fact.drop_duplicate_facts
     2.8                  |> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t
     2.9                  |> map (nickname_of_thm o snd)
    2.10              in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Oct 17 23:41:00 2013 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Oct 18 00:05:31 2013 +0200
     3.3 @@ -544,7 +544,8 @@
     3.4             val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
     3.5             val facts =
     3.6               all_facts ctxt false ho_atp reserved add chained css
     3.7 -             |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
     3.8 +             |> filter_out ((member Thm.eq_thm_prop del orf
     3.9 +               (No_ATPs.member ctxt andf not o member Thm.eq_thm_prop add)) o snd)
    3.10           in
    3.11             facts
    3.12           end)
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 17 23:41:00 2013 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 18 00:05:31 2013 +0200
     4.3 @@ -1317,16 +1317,19 @@
     4.4               if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
     4.5            else
     4.6              (false, mepoN)
     4.7 +
     4.8 +      val unique_facts = drop_duplicate_facts facts
     4.9        val add_ths = Attrib.eval_thms ctxt add
    4.10 +
    4.11        fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
    4.12        fun add_and_take accepts =
    4.13          (case add_ths of
    4.14             [] => accepts
    4.15 -         | _ => (facts |> filter in_add |> map fact_of_raw_fact) @
    4.16 +         | _ => (unique_facts |> filter in_add |> map fact_of_raw_fact) @
    4.17                  (accepts |> filter_out in_add))
    4.18          |> take max_facts
    4.19        fun mepo () =
    4.20 -        (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t facts
    4.21 +        (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts
    4.22           |> weight_facts_steeply, [])
    4.23        fun mash () =
    4.24          mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Oct 17 23:41:00 2013 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Oct 18 00:05:31 2013 +0200
     5.3 @@ -439,7 +439,6 @@
     5.4          (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t =
     5.5    let
     5.6      val thy = Proof_Context.theory_of ctxt
     5.7 -    val facts = drop_duplicate_facts facts
     5.8      val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
     5.9      val add_pconsts = add_pconsts_in_term thy
    5.10      val chained_ts =