4 |
4 |
5 structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = |
5 structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = |
6 struct |
6 struct |
7 |
7 |
8 val relevance_filter_args = |
8 val relevance_filter_args = |
9 [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq), |
9 [("worse_irrel_freq", Sledgehammer_Filter.worse_irrel_freq), |
10 ("higher_order_irrel_weight", |
10 ("higher_order_irrel_weight", Sledgehammer_Filter.higher_order_irrel_weight), |
11 Sledgehammer_Fact_Filter.higher_order_irrel_weight), |
11 ("abs_rel_weight", Sledgehammer_Filter.abs_rel_weight), |
12 ("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight), |
12 ("abs_irrel_weight", Sledgehammer_Filter.abs_irrel_weight), |
13 ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight), |
13 ("skolem_irrel_weight", Sledgehammer_Filter.skolem_irrel_weight), |
14 ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight), |
14 ("intro_bonus", Sledgehammer_Filter.intro_bonus), |
15 ("intro_bonus", Sledgehammer_Fact_Filter.intro_bonus), |
15 ("elim_bonus", Sledgehammer_Filter.elim_bonus), |
16 ("elim_bonus", Sledgehammer_Fact_Filter.elim_bonus), |
16 ("simp_bonus", Sledgehammer_Filter.simp_bonus), |
17 ("simp_bonus", Sledgehammer_Fact_Filter.simp_bonus), |
17 ("local_bonus", Sledgehammer_Filter.local_bonus), |
18 ("local_bonus", Sledgehammer_Fact_Filter.local_bonus), |
18 ("chained_bonus", Sledgehammer_Filter.chained_bonus), |
19 ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus), |
19 ("max_imperfect", Sledgehammer_Filter.max_imperfect), |
20 ("max_imperfect", Sledgehammer_Fact_Filter.max_imperfect), |
20 ("max_imperfect_exp", Sledgehammer_Filter.max_imperfect_exp), |
21 ("max_imperfect_exp", Sledgehammer_Fact_Filter.max_imperfect_exp), |
21 ("threshold_divisor", Sledgehammer_Filter.threshold_divisor), |
22 ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor), |
22 ("ridiculous_threshold", Sledgehammer_Filter.ridiculous_threshold)] |
23 ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold)] |
|
24 |
23 |
25 structure Prooftab = |
24 structure Prooftab = |
26 Table(type key = int * int val ord = prod_ord int_ord int_ord); |
25 Table(type key = int * int val ord = prod_ord int_ord int_ord); |
27 |
26 |
28 val proof_table = Unsynchronized.ref Prooftab.empty |
27 val proof_table = Unsynchronized.ref Prooftab.empty |
102 val {relevance_thresholds, full_types, max_relevant, theory_relevant, |
101 val {relevance_thresholds, full_types, max_relevant, theory_relevant, |
103 ...} = Sledgehammer_Isar.default_params thy args |
102 ...} = Sledgehammer_Isar.default_params thy args |
104 val subgoal = 1 |
103 val subgoal = 1 |
105 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal |
104 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal |
106 val facts = |
105 val facts = |
107 Sledgehammer_Fact_Filter.relevant_facts ctxt full_types |
106 Sledgehammer_Filter.relevant_facts ctxt full_types |
108 relevance_thresholds |
107 relevance_thresholds |
109 (the_default default_max_relevant max_relevant) |
108 (the_default default_max_relevant max_relevant) |
110 (the_default false theory_relevant) |
109 (the_default false theory_relevant) |
111 {add = [], del = [], only = false} facts hyp_ts concl_t |
110 {add = [], del = [], only = false} facts hyp_ts concl_t |
112 |> map (fst o fst) |
111 |> map (fst o fst) |