equal
deleted
inserted
replaced
195 fun steep_weight_of_fact rank = Math.pow (0.62, log2 (Real.fromInt (rank + 1))) (* FUDGE *) |
195 fun steep_weight_of_fact rank = Math.pow (0.62, log2 (Real.fromInt (rank + 1))) (* FUDGE *) |
196 |
196 |
197 fun weight_facts_smoothly facts = facts ~~ map smooth_weight_of_fact (0 upto length facts - 1) |
197 fun weight_facts_smoothly facts = facts ~~ map smooth_weight_of_fact (0 upto length facts - 1) |
198 fun weight_facts_steeply facts = facts ~~ map steep_weight_of_fact (0 upto length facts - 1) |
198 fun weight_facts_steeply facts = facts ~~ map steep_weight_of_fact (0 upto length facts - 1) |
199 |
199 |
200 fun rev_sort_array_prefix cmp bnd a = |
200 fun sort_array_suffix cmp needed a = |
201 let |
201 let |
202 exception BOTTOM of int |
202 exception BOTTOM of int |
203 |
203 |
204 val al = Array.length a |
204 val al = Array.length a |
205 |
205 |
244 end |
244 end |
245 |
245 |
246 fun for i = if i < 0 then () else (trickle al i (Array.sub (a, i)); for (i - 1)) |
246 fun for i = if i < 0 then () else (trickle al i (Array.sub (a, i)); for (i - 1)) |
247 |
247 |
248 fun for2 i = |
248 fun for2 i = |
249 if i < Integer.max 2 (al - bnd) then |
249 if i < Integer.max 2 (al - needed) then |
250 () |
250 () |
251 else |
251 else |
252 let val e = Array.sub (a, i) in |
252 let val e = Array.sub (a, i) in |
253 Array.update (a, i, Array.sub (a, 0)); |
253 Array.update (a, i, Array.sub (a, 0)); |
254 trickleup (bubble i 0) e; |
254 trickleup (bubble i 0) e; |
264 end |
264 end |
265 else |
265 else |
266 () |
266 () |
267 end |
267 end |
268 |
268 |
269 fun rev_sort_list_prefix cmp bnd xs = |
269 fun rev_sort_list_prefix cmp needed xs = |
270 let val ary = Array.fromList xs in |
270 let val ary = Array.fromList xs in |
271 rev_sort_array_prefix cmp bnd ary; |
271 sort_array_suffix cmp needed ary; |
272 Array.foldr (op ::) [] ary |
272 Array.foldl (op ::) [] ary |
273 end |
273 end |
274 |
274 |
275 |
275 |
276 (*** Isabelle-agnostic machine learning ***) |
276 (*** Isabelle-agnostic machine learning ***) |
277 |
277 |
361 |
361 |
362 fun ret at acc = |
362 fun ret at acc = |
363 if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc) |
363 if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc) |
364 in |
364 in |
365 select_visible_facts 100000.0 posterior visible_facts; |
365 select_visible_facts 100000.0 posterior visible_facts; |
366 rev_sort_array_prefix (Real.compare o pairself snd) max_suggs posterior; |
366 sort_array_suffix (Real.compare o pairself snd) max_suggs posterior; |
367 ret (Integer.max 0 (num_facts - max_suggs)) [] |
367 ret (Integer.max 0 (num_facts - max_suggs)) [] |
368 end |
368 end |
369 |
369 |
370 val initial_number_of_nearest_neighbors = 1 |
370 val initial_number_of_nearest_neighbors = 1 |
371 |
371 |
394 in |
394 in |
395 List.app inc_overlap (Array.sub (feat_facts, s)) |
395 List.app inc_overlap (Array.sub (feat_facts, s)) |
396 end |
396 end |
397 |
397 |
398 val _ = List.app do_feat goal_feats |
398 val _ = List.app do_feat goal_feats |
399 val _ = rev_sort_array_prefix (Real.compare o pairself snd) num_facts overlaps_sqr |
399 val _ = sort_array_suffix (Real.compare o pairself snd) num_facts overlaps_sqr |
400 val no_recommends = Unsynchronized.ref 0 |
400 val no_recommends = Unsynchronized.ref 0 |
401 val recommends = Array.tabulate (num_facts, rpair 0.0) |
401 val recommends = Array.tabulate (num_facts, rpair 0.0) |
402 val age = Unsynchronized.ref 500000000.0 |
402 val age = Unsynchronized.ref 500000000.0 |
403 |
403 |
404 fun inc_recommend v j = |
404 fun inc_recommend v j = |
436 if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1) |
436 if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1) |
437 in |
437 in |
438 while1 (); |
438 while1 (); |
439 while2 (); |
439 while2 (); |
440 select_visible_facts 1000000000.0 recommends visible_facts; |
440 select_visible_facts 1000000000.0 recommends visible_facts; |
441 rev_sort_array_prefix (Real.compare o pairself snd) max_suggs recommends; |
441 sort_array_suffix (Real.compare o pairself snd) max_suggs recommends; |
442 ret [] (Integer.max 0 (num_facts - max_suggs)) |
442 ret [] (Integer.max 0 (num_facts - max_suggs)) |
443 end |
443 end |
444 |
444 |
445 (* experimental *) |
445 (* experimental *) |
446 fun external_tool tool max_suggs learns goal_feats = |
446 fun external_tool tool max_suggs learns goal_feats = |
1124 |
1124 |
1125 val chained_feature_factor = 0.5 (* FUDGE *) |
1125 val chained_feature_factor = 0.5 (* FUDGE *) |
1126 val extra_feature_factor = 0.1 (* FUDGE *) |
1126 val extra_feature_factor = 0.1 (* FUDGE *) |
1127 val num_extra_feature_facts = 10 (* FUDGE *) |
1127 val num_extra_feature_facts = 10 (* FUDGE *) |
1128 |
1128 |
1129 val max_proximity_facts = 100 |
1129 val max_proximity_facts = 100 (* FUDGE *) |
1130 |
1130 |
1131 fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown = |
1131 fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown = |
1132 let |
1132 let |
1133 val inter_fact = inter (eq_snd Thm.eq_thm_prop) |
1133 val inter_fact = inter (eq_snd Thm.eq_thm_prop) |
1134 val raw_mash = find_suggested_facts ctxt facts suggs |
1134 val raw_mash = find_suggested_facts ctxt facts suggs |