further speed up duplicate elimination
authorblanchet
Tue Oct 08 14:53:33 2013 +0200 (2013-10-08 ago)
changeset 54077af65902b6e30
parent 54076 5337fd7d53c9
child 54078 1d371c3f2703
further speed up duplicate elimination
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 14:41:25 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 14:53:33 2013 +0200
     1.3 @@ -102,6 +102,7 @@
     1.4                       body_type T = @{typ bool}
     1.5                     | _ => false)
     1.6  
     1.7 +(* TODO: get rid of *)
     1.8  fun normalize_vars t =
     1.9    let
    1.10      fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
    1.11 @@ -377,19 +378,13 @@
    1.12      val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
    1.13    in (plain_name_tab, inclass_name_tab) end
    1.14  
    1.15 -fun keyed_distinct key1_of key2_of ths =
    1.16 +fun fact_distinct thy facts =
    1.17    fold (fn fact as (_, th) =>
    1.18 -      Net.insert_term_safe (op aconv o pairself (key2_of o key1_of o prop_of o snd)) (key1_of (prop_of th), fact))
    1.19 -    ths Net.empty
    1.20 +      Net.insert_term_safe (Pattern.equiv thy o pairself (normalize_eq o prop_of o snd))
    1.21 +        (normalize_eq (prop_of th), fact))
    1.22 +    facts Net.empty
    1.23    |> Net.entries
    1.24  
    1.25 -fun hashed_keyed_distinct hash_of key1_of key2_of facts =
    1.26 -  let
    1.27 -    val ys = map (`(hash_of o prop_of o snd)) facts
    1.28 -    val sorted_ys = sort (int_ord o pairself fst) ys
    1.29 -    val grouped_ys = AList.coalesce (op =) sorted_ys
    1.30 -  in maps (keyed_distinct key1_of key2_of o snd) grouped_ys end
    1.31 -
    1.32  fun struct_induct_rule_on th =
    1.33    case Logic.strip_horn (prop_of th) of
    1.34      (prems, @{const Trueprop}
    1.35 @@ -534,6 +529,7 @@
    1.36      []
    1.37    else
    1.38      let
    1.39 +      val thy = Proof_Context.theory_of ctxt
    1.40        val chained =
    1.41          chained
    1.42          |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
    1.43 @@ -545,7 +541,7 @@
    1.44           let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    1.45             all_facts ctxt false ho_atp reserved add chained css
    1.46             |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
    1.47 -           |> hashed_keyed_distinct size_of_term normalize_eq normalize_vars
    1.48 +           |> fact_distinct thy
    1.49           end)
    1.50        |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    1.51      end