9 sig |
9 sig |
10 type stature = ATP_Problem_Generate.stature |
10 type stature = ATP_Problem_Generate.stature |
11 type raw_fact = Sledgehammer_Fact.raw_fact |
11 type raw_fact = Sledgehammer_Fact.raw_fact |
12 type fact = Sledgehammer_Fact.fact |
12 type fact = Sledgehammer_Fact.fact |
13 type params = Sledgehammer_Provers.params |
13 type params = Sledgehammer_Provers.params |
14 type relevance_fudge = Sledgehammer_Provers.relevance_fudge |
14 |
|
15 type relevance_fudge = |
|
16 {local_const_multiplier : real, |
|
17 worse_irrel_freq : real, |
|
18 higher_order_irrel_weight : real, |
|
19 abs_rel_weight : real, |
|
20 abs_irrel_weight : real, |
|
21 theory_const_rel_weight : real, |
|
22 theory_const_irrel_weight : real, |
|
23 chained_const_irrel_weight : real, |
|
24 intro_bonus : real, |
|
25 elim_bonus : real, |
|
26 simp_bonus : real, |
|
27 local_bonus : real, |
|
28 assum_bonus : real, |
|
29 chained_bonus : real, |
|
30 max_imperfect : real, |
|
31 max_imperfect_exp : real, |
|
32 threshold_divisor : real, |
|
33 ridiculous_threshold : real} |
15 |
34 |
16 val trace : bool Config.T |
35 val trace : bool Config.T |
17 val pseudo_abs_name : string |
36 val pseudo_abs_name : string |
|
37 val default_relevance_fudge : relevance_fudge |
18 val mepo_suggested_facts : |
38 val mepo_suggested_facts : |
19 Proof.context -> params -> string -> int -> relevance_fudge option |
39 Proof.context -> params -> int -> relevance_fudge option -> term list -> term -> |
20 -> term list -> term -> raw_fact list -> fact list |
40 raw_fact list -> fact list |
21 end; |
41 end; |
22 |
42 |
23 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO = |
43 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO = |
24 struct |
44 struct |
25 |
45 |
33 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
53 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
34 |
54 |
35 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator |
55 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator |
36 val pseudo_abs_name = sledgehammer_prefix ^ "abs" |
56 val pseudo_abs_name = sledgehammer_prefix ^ "abs" |
37 val theory_const_suffix = Long_Name.separator ^ " 1" |
57 val theory_const_suffix = Long_Name.separator ^ " 1" |
|
58 |
|
59 type relevance_fudge = |
|
60 {local_const_multiplier : real, |
|
61 worse_irrel_freq : real, |
|
62 higher_order_irrel_weight : real, |
|
63 abs_rel_weight : real, |
|
64 abs_irrel_weight : real, |
|
65 theory_const_rel_weight : real, |
|
66 theory_const_irrel_weight : real, |
|
67 chained_const_irrel_weight : real, |
|
68 intro_bonus : real, |
|
69 elim_bonus : real, |
|
70 simp_bonus : real, |
|
71 local_bonus : real, |
|
72 assum_bonus : real, |
|
73 chained_bonus : real, |
|
74 max_imperfect : real, |
|
75 max_imperfect_exp : real, |
|
76 threshold_divisor : real, |
|
77 ridiculous_threshold : real} |
|
78 |
|
79 (* FUDGE *) |
|
80 val default_relevance_fudge = |
|
81 {local_const_multiplier = 1.5, |
|
82 worse_irrel_freq = 100.0, |
|
83 higher_order_irrel_weight = 1.05, |
|
84 abs_rel_weight = 0.5, |
|
85 abs_irrel_weight = 2.0, |
|
86 theory_const_rel_weight = 0.5, |
|
87 theory_const_irrel_weight = 0.25, |
|
88 chained_const_irrel_weight = 0.25, |
|
89 intro_bonus = 0.15, |
|
90 elim_bonus = 0.15, |
|
91 simp_bonus = 0.15, |
|
92 local_bonus = 0.55, |
|
93 assum_bonus = 1.05, |
|
94 chained_bonus = 1.5, |
|
95 max_imperfect = 11.5, |
|
96 max_imperfect_exp = 1.0, |
|
97 threshold_divisor = 2.0, |
|
98 ridiculous_threshold = 0.1} |
38 |
99 |
39 fun order_of_type (Type (@{type_name fun}, [T1, T2])) = |
100 fun order_of_type (Type (@{type_name fun}, [T1, T2])) = |
40 Int.max (order_of_type T1 + 1, order_of_type T2) |
101 Int.max (order_of_type T1 + 1, order_of_type T2) |
41 | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0 |
102 | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0 |
42 | order_of_type _ = 0 |
103 | order_of_type _ = 0 |
495 |> insert_special_facts |
556 |> insert_special_facts |
496 |> tap (fn accepts => trace_msg ctxt (fn () => |
557 |> tap (fn accepts => trace_msg ctxt (fn () => |
497 "Total relevant: " ^ string_of_int (length accepts))) |
558 "Total relevant: " ^ string_of_int (length accepts))) |
498 end |
559 end |
499 |
560 |
500 fun mepo_suggested_facts ctxt |
561 fun mepo_suggested_facts ctxt ({fact_thresholds = (thres0, thres1), ...} : params) max_facts fudge |
501 ({fact_thresholds = (thres0, thres1), ...} : params) prover |
562 hyp_ts concl_t facts = |
502 max_facts fudge hyp_ts concl_t facts = |
|
503 let |
563 let |
504 val thy = Proof_Context.theory_of ctxt |
564 val thy = Proof_Context.theory_of ctxt |
505 val fudge = |
565 val fudge = fudge |> the_default default_relevance_fudge |
506 case fudge of |
|
507 SOME fudge => fudge |
|
508 | NONE => Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover |
|
509 val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0), |
566 val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0), |
510 1.0 / Real.fromInt (max_facts + 1)) |
567 1.0 / Real.fromInt (max_facts + 1)) |
511 in |
568 in |
512 trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ " facts"); |
569 trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ " facts"); |
513 (if thres1 < 0.0 then |
570 (if thres1 < 0.0 then |