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 val scale_factor = 1000 |
128 (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *) |
129 |
129 fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0 |
130 fun scaled_powX x = Integer.pow 8 x |
|
131 |
130 |
132 fun sum_sq_avg [] = 0 |
131 fun sum_sq_avg [] = 0 |
133 | sum_sq_avg xs = fold (Integer.add o scaled_powX) xs 0 div (length xs) |
132 | sum_sq_avg xs = |
|
133 Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs |
134 |
134 |
135 fun mesh_facts max_facts [(selected, unknown)] = |
135 fun mesh_facts max_facts [(selected, unknown)] = |
136 take max_facts selected @ take (max_facts - length selected) unknown |
136 take max_facts selected @ take (max_facts - length selected) unknown |
137 | mesh_facts max_facts mess = |
137 | mesh_facts max_facts mess = |
138 let |
138 let |
139 val mess = mess |> map (apfst (`length)) |
139 val mess = mess |> map (apfst (`length)) |
140 val fact_eq = Thm.eq_thm o pairself snd |
140 val fact_eq = Thm.eq_thm o pairself snd |
141 fun score_in fact ((sel_len, sels), unks) = |
141 fun score_in fact ((sel_len, sels), unks) = |
142 case find_index (curry fact_eq fact) sels of |
142 case find_index (curry fact_eq fact) sels of |
143 ~1 => (case find_index (curry fact_eq fact) unks of |
143 ~1 => (case find_index (curry fact_eq fact) unks of |
144 ~1 => SOME 0 |
144 ~1 => SOME sel_len |
145 | _ => NONE) |
145 | _ => NONE) |
146 | j => SOME (scale_factor * (sel_len - j) div sel_len) |
146 | j => SOME j |
147 fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg |
147 fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg |
148 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 [] |
149 in |
149 in |
150 facts |> map (`score_of) |> sort (int_ord o swap o pairself fst) |
150 facts |> map (`score_of) |> sort (int_ord o swap o pairself fst) |
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 |
151 |> map snd |> take max_facts |
154 end |
152 end |
155 |
153 |
156 val thy_feature_prefix = "y_" |
154 val thy_feature_prefix = "y_" |
157 |
155 |