364 fun fact_weight fudge loc const_tab relevant_consts fact_consts = |
364 fun fact_weight fudge loc const_tab relevant_consts fact_consts = |
365 case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts) |
365 case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts) |
366 ||> filter_out (pconst_hyper_mem swap relevant_consts) of |
366 ||> filter_out (pconst_hyper_mem swap relevant_consts) of |
367 ([], _) => 0.0 |
367 ([], _) => 0.0 |
368 | (rel, irrel) => |
368 | (rel, irrel) => |
369 let |
369 if forall (forall (String.isSuffix theory_const_suffix o fst)) |
370 val irrel = irrel |> filter_out (pconst_mem swap rel) |
370 [rel, irrel] then |
371 val rel_weight = |
371 0.0 |
372 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel |
372 else |
373 val irrel_weight = |
373 let |
374 ~ (locality_bonus fudge loc) |
374 val irrel = irrel |> filter_out (pconst_mem swap rel) |
375 |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel |
375 val rel_weight = |
376 val res = rel_weight / (rel_weight + irrel_weight) |
376 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel |
377 in if Real.isFinite res then res else 0.0 end |
377 val irrel_weight = |
|
378 ~ (locality_bonus fudge loc) |
|
379 |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel |
|
380 val res = rel_weight / (rel_weight + irrel_weight) |
|
381 in if Real.isFinite res then res else 0.0 end |
378 |
382 |
379 fun pconsts_in_fact thy is_built_in_const t = |
383 fun pconsts_in_fact thy is_built_in_const t = |
380 Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) |
384 Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) |
381 (pconsts_in_terms thy is_built_in_const true (SOME true) [t]) [] |
385 (pconsts_in_terms thy is_built_in_const true (SOME true) [t]) [] |
382 fun pair_consts_fact thy is_built_in_const fudge fact = |
386 fun pair_consts_fact thy is_built_in_const fudge fact = |