3 *) |
3 *) |
4 |
4 |
5 structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = |
5 structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = |
6 struct |
6 struct |
7 |
7 |
8 structure SF = Sledgehammer_Filter |
8 fun get args name default_value = |
|
9 case AList.lookup (op =) args name of |
|
10 SOME value => the (Real.fromString value) |
|
11 | NONE => default_value |
9 |
12 |
10 val relevance_filter_args = |
13 fun extract_relevance_fudge args |
11 [("worse_irrel_freq", SF.worse_irrel_freq), |
14 {worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight, |
12 ("higher_order_irrel_weight", SF.higher_order_irrel_weight), |
15 abs_irrel_weight, skolem_irrel_weight, theory_const_rel_weight, |
13 ("abs_rel_weight", SF.abs_rel_weight), |
16 theory_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, |
14 ("abs_irrel_weight", SF.abs_irrel_weight), |
17 local_bonus, assum_bonus, chained_bonus, max_imperfect, |
15 ("skolem_irrel_weight", SF.skolem_irrel_weight), |
18 max_imperfect_exp, threshold_divisor, ridiculous_threshold} = |
16 ("theory_const_rel_weight", SF.theory_const_rel_weight), |
19 {worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, |
17 ("theory_const_irrel_weight", SF.theory_const_irrel_weight), |
20 higher_order_irrel_weight = |
18 ("intro_bonus", SF.intro_bonus), |
21 get args "higher_order_irrel_weight" higher_order_irrel_weight, |
19 ("elim_bonus", SF.elim_bonus), |
22 abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, |
20 ("simp_bonus", SF.simp_bonus), |
23 abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, |
21 ("local_bonus", SF.local_bonus), |
24 skolem_irrel_weight = get args "skolem_irrel_weight" skolem_irrel_weight, |
22 ("assum_bonus", SF.assum_bonus), |
25 theory_const_rel_weight = |
23 ("chained_bonus", SF.chained_bonus), |
26 get args "theory_const_rel_weight" theory_const_rel_weight, |
24 ("max_imperfect", SF.max_imperfect), |
27 theory_const_irrel_weight = |
25 ("max_imperfect_exp", SF.max_imperfect_exp), |
28 get args "theory_const_irrel_weight" theory_const_irrel_weight, |
26 ("threshold_divisor", SF.threshold_divisor), |
29 intro_bonus = get args "intro_bonus" intro_bonus, |
27 ("ridiculous_threshold", SF.ridiculous_threshold)] |
30 elim_bonus = get args "elim_bonus" elim_bonus, |
|
31 simp_bonus = get args "simp_bonus" simp_bonus, |
|
32 local_bonus = get args "local_bonus" local_bonus, |
|
33 assum_bonus = get args "assum_bonus" assum_bonus, |
|
34 chained_bonus = get args "chained_bonus" chained_bonus, |
|
35 max_imperfect = get args "max_imperfect" max_imperfect, |
|
36 max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp, |
|
37 threshold_divisor = get args "threshold_divisor" threshold_divisor, |
|
38 ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold} |
28 |
39 |
29 structure Prooftab = |
40 structure Prooftab = |
30 Table(type key = int * int val ord = prod_ord int_ord int_ord); |
41 Table(type key = int * int val ord = prod_ord int_ord int_ord); |
31 |
42 |
32 val proof_table = Unsynchronized.ref Prooftab.empty |
43 val proof_table = Unsynchronized.ref Prooftab.empty |
83 "%")) |
94 "%")) |
84 else |
95 else |
85 () |
96 () |
86 |
97 |
87 val default_max_relevant = 300 |
98 val default_max_relevant = 300 |
|
99 val prover_name = ATP_Systems.eN (* arbitrary ATP *) |
88 |
100 |
89 fun with_index (i, s) = s ^ "@" ^ string_of_int i |
101 fun with_index (i, s) = s ^ "@" ^ string_of_int i |
90 |
102 |
91 fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) = |
103 fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) = |
92 case (Position.line_of pos, Position.column_of pos) of |
104 case (Position.line_of pos, Position.column_of pos) of |
93 (SOME line_num, SOME col_num) => |
105 (SOME line_num, SOME col_num) => |
94 (case Prooftab.lookup (!proof_table) (line_num, col_num) of |
106 (case Prooftab.lookup (!proof_table) (line_num, col_num) of |
95 SOME proofs => |
107 SOME proofs => |
96 let |
108 let |
97 val {context = ctxt, facts, goal} = Proof.goal pre |
109 val {context = ctxt, facts, goal} = Proof.goal pre |
98 val args = |
110 val relevance_fudge = |
99 args |
111 extract_relevance_fudge args |
100 |> filter (fn (key, value) => |
112 (Sledgehammer.relevance_fudge_for_prover prover_name) |
101 case AList.lookup (op =) relevance_filter_args key of |
|
102 SOME rf => (rf := the (Real.fromString value); false) |
|
103 | NONE => true) |
|
104 |
|
105 val {relevance_thresholds, full_types, max_relevant, ...} = |
113 val {relevance_thresholds, full_types, max_relevant, ...} = |
106 Sledgehammer_Isar.default_params ctxt args |
114 Sledgehammer_Isar.default_params ctxt args |
107 val subgoal = 1 |
115 val subgoal = 1 |
108 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal |
116 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal |
109 val facts = |
117 val facts = |
110 SF.relevant_facts ctxt full_types |
118 Sledgehammer_Filter.relevant_facts ctxt full_types |
111 relevance_thresholds |
119 relevance_thresholds |
112 (the_default default_max_relevant max_relevant) |
120 (the_default default_max_relevant max_relevant) relevance_fudge |
113 {add = [], del = [], only = false} facts hyp_ts concl_t |
121 {add = [], del = [], only = false} facts hyp_ts concl_t |
114 |> map (fst o fst) |
122 |> map (fst o fst) |
115 val (found_facts, lost_facts) = |
123 val (found_facts, lost_facts) = |
116 List.concat proofs |> sort_distinct string_ord |
124 List.concat proofs |> sort_distinct string_ord |
117 |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |
125 |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |