faster uniquification
authorblanchet
Tue Sep 10 15:56:51 2013 +0200 (2013-09-10 ago)
changeset 535049750618c32ed
parent 53503 d2f21e305d0c
child 53505 412f8c590c6c
faster uniquification
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.3 @@ -385,10 +385,17 @@
     1.4      val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
     1.5    in (plain_name_tab, inclass_name_tab) end
     1.6  
     1.7 -fun uniquify facts =
     1.8 -  Termtab.fold (cons o snd)
     1.9 -      (fold (Termtab.default o `(normalize_eq_vars o prop_of o snd)) facts
    1.10 -            Termtab.empty) []
    1.11 +fun keyed_distinct key_of xs =
    1.12 +  let val tab = fold (Termtab.default o `key_of) xs Termtab.empty in
    1.13 +    Termtab.fold (cons o snd) tab []
    1.14 +  end
    1.15 +
    1.16 +fun hashed_keyed_distinct hash_of key_of xs =
    1.17 +  let
    1.18 +    val ys = map (`hash_of) xs
    1.19 +    val sorted_ys = sort (int_ord o pairself fst) ys
    1.20 +    val grouped_ys = AList.coalesce (op =) sorted_ys
    1.21 +  in maps (keyed_distinct key_of o snd) grouped_ys end
    1.22  
    1.23  fun struct_induct_rule_on th =
    1.24    case Logic.strip_horn (prop_of th) of
    1.25 @@ -540,7 +547,8 @@
    1.26             all_facts ctxt false ho_atp reserved add chained css
    1.27             |> filter_out (member Thm.eq_thm_prop del o snd)
    1.28             |> maybe_filter_no_atps ctxt
    1.29 -           |> uniquify
    1.30 +           |> hashed_keyed_distinct (size_of_term o prop_of o snd)
    1.31 +                  (normalize_eq_vars o prop_of o snd)
    1.32           end)
    1.33        |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    1.34      end