1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -125,27 +125,32 @@
     1.4    find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
     1.5  fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
     1.6  
     1.7 -fun sum_avg _ [] = 1000000000 (* big number *)
     1.8 -  | sum_avg n xs = fold (Integer.add o Integer.mult n) xs 0 div (length xs)
     1.9 +val scale_factor = 1000
    1.10 +
    1.11 +fun scaled_powX x = Integer.pow 8 x
    1.12 +
    1.13 +fun sum_sq_avg [] = 0
    1.14 +  | sum_sq_avg xs = fold (Integer.add o scaled_powX) xs 0 div (length xs)
    1.15  
    1.16  fun mesh_facts max_facts [(selected, unknown)] =
    1.17      take max_facts selected @ take (max_facts - length selected) unknown
    1.18    | mesh_facts max_facts mess =
    1.19      let
    1.20        val mess = mess |> map (apfst (`length))
    1.21 -      val n = length mess
    1.22        val fact_eq = Thm.eq_thm o pairself snd
    1.23        fun score_in fact ((sel_len, sels), unks) =
    1.24          case find_index (curry fact_eq fact) sels of
    1.25            ~1 => (case find_index (curry fact_eq fact) unks of
    1.26 -                   ~1 => SOME sel_len
    1.27 +                   ~1 => SOME 0
    1.28                   | _ => NONE)
    1.29 -        | j => SOME j
    1.30 -      fun score_of fact = mess |> map_filter (score_in fact) |> sum_avg n
    1.31 +        | j => SOME (scale_factor * (sel_len - j) div sel_len)
    1.32 +      fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg
    1.33        val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
    1.34      in
    1.35 -      facts |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
    1.36 -            |> take max_facts
    1.37 +      facts |> map (`score_of) |> sort (int_ord o swap o pairself fst)
    1.38 +|> tap (List.app (fn (score, (_, th)) => tracing ("score: " ^ string_of_int score ^ " " ^ Thm.get_name_hint th))
    1.39 +)
    1.40 +            |> map snd |> take max_facts
    1.41      end
    1.42  
    1.43  val thy_feature_prefix = "y_"