src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
changeset 48328 ca0b7d19dd62
parent 48327 568b3193e53e
child 48329 5781c4620245
equal deleted inserted replaced
48327:568b3193e53e 48328:ca0b7d19dd62
   123 
   123 
   124 fun find_suggested facts sugg =
   124 fun find_suggested facts sugg =
   125   find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
   125   find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
   126 fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
   126 fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
   127 
   127 
   128 fun sum_avg _ [] = 1000000000 (* big number *)
   128 val scale_factor = 1000
   129   | sum_avg n xs = fold (Integer.add o Integer.mult n) xs 0 div (length xs)
   129 
       
   130 fun scaled_powX x = Integer.pow 8 x
       
   131 
       
   132 fun sum_sq_avg [] = 0
       
   133   | sum_sq_avg xs = fold (Integer.add o scaled_powX) xs 0 div (length xs)
   130 
   134 
   131 fun mesh_facts max_facts [(selected, unknown)] =
   135 fun mesh_facts max_facts [(selected, unknown)] =
   132     take max_facts selected @ take (max_facts - length selected) unknown
   136     take max_facts selected @ take (max_facts - length selected) unknown
   133   | mesh_facts max_facts mess =
   137   | mesh_facts max_facts mess =
   134     let
   138     let
   135       val mess = mess |> map (apfst (`length))
   139       val mess = mess |> map (apfst (`length))
   136       val n = length mess
       
   137       val fact_eq = Thm.eq_thm o pairself snd
   140       val fact_eq = Thm.eq_thm o pairself snd
   138       fun score_in fact ((sel_len, sels), unks) =
   141       fun score_in fact ((sel_len, sels), unks) =
   139         case find_index (curry fact_eq fact) sels of
   142         case find_index (curry fact_eq fact) sels of
   140           ~1 => (case find_index (curry fact_eq fact) unks of
   143           ~1 => (case find_index (curry fact_eq fact) unks of
   141                    ~1 => SOME sel_len
   144                    ~1 => SOME 0
   142                  | _ => NONE)
   145                  | _ => NONE)
   143         | j => SOME j
   146         | j => SOME (scale_factor * (sel_len - j) div sel_len)
   144       fun score_of fact = mess |> map_filter (score_in fact) |> sum_avg n
   147       fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg
   145       val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
   148       val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
   146     in
   149     in
   147       facts |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
   150       facts |> map (`score_of) |> sort (int_ord o swap o pairself fst)
   148             |> take max_facts
   151 |> tap (List.app (fn (score, (_, th)) => tracing ("score: " ^ string_of_int score ^ " " ^ Thm.get_name_hint th))
       
   152 )
       
   153             |> map snd |> take max_facts
   149     end
   154     end
   150 
   155 
   151 val thy_feature_prefix = "y_"
   156 val thy_feature_prefix = "y_"
   152 
   157 
   153 val thy_feature_name_of = prefix thy_feature_prefix
   158 val thy_feature_name_of = prefix thy_feature_prefix