10 SOME value => Markup.parse_real value |
10 SOME value => Markup.parse_real value |
11 | NONE => default_value |
11 | NONE => default_value |
12 |
12 |
13 fun extract_relevance_fudge args |
13 fun extract_relevance_fudge args |
14 {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, |
14 {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, |
15 abs_rel_weight, abs_irrel_weight, skolem_irrel_weight, |
15 abs_rel_weight, abs_irrel_weight, theory_const_rel_weight, |
16 theory_const_rel_weight, theory_const_irrel_weight, |
16 theory_const_irrel_weight, chained_const_irrel_weight, intro_bonus, |
17 chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, |
17 elim_bonus, simp_bonus, local_bonus, assum_bonus, chained_bonus, |
18 local_bonus, assum_bonus, chained_bonus, max_imperfect, max_imperfect_exp, |
18 max_imperfect, max_imperfect_exp, threshold_divisor, |
19 threshold_divisor, ridiculous_threshold} = |
19 ridiculous_threshold} = |
20 {local_const_multiplier = |
20 {local_const_multiplier = |
21 get args "local_const_multiplier" local_const_multiplier, |
21 get args "local_const_multiplier" local_const_multiplier, |
22 worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, |
22 worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, |
23 higher_order_irrel_weight = |
23 higher_order_irrel_weight = |
24 get args "higher_order_irrel_weight" higher_order_irrel_weight, |
24 get args "higher_order_irrel_weight" higher_order_irrel_weight, |
25 abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, |
25 abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, |
26 abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, |
26 abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, |
27 skolem_irrel_weight = get args "skolem_irrel_weight" skolem_irrel_weight, |
|
28 theory_const_rel_weight = |
27 theory_const_rel_weight = |
29 get args "theory_const_rel_weight" theory_const_rel_weight, |
28 get args "theory_const_rel_weight" theory_const_rel_weight, |
30 theory_const_irrel_weight = |
29 theory_const_irrel_weight = |
31 get args "theory_const_irrel_weight" theory_const_irrel_weight, |
30 get args "theory_const_irrel_weight" theory_const_irrel_weight, |
32 chained_const_irrel_weight = |
31 chained_const_irrel_weight = |