equal
deleted
inserted
replaced
5 Sledgehammer's relevance filter. |
5 Sledgehammer's relevance filter. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_FILTER = |
8 signature SLEDGEHAMMER_FILTER = |
9 sig |
9 sig |
10 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained |
10 type locality = ATP_Translate.locality |
11 |
11 |
12 type relevance_fudge = |
12 type relevance_fudge = |
13 {local_const_multiplier : real, |
13 {local_const_multiplier : real, |
14 worse_irrel_freq : real, |
14 worse_irrel_freq : real, |
15 higher_order_irrel_weight : real, |
15 higher_order_irrel_weight : real, |
37 |
37 |
38 val trace : bool Config.T |
38 val trace : bool Config.T |
39 val new_monomorphizer : bool Config.T |
39 val new_monomorphizer : bool Config.T |
40 val ignore_no_atp : bool Config.T |
40 val ignore_no_atp : bool Config.T |
41 val instantiate_inducts : bool Config.T |
41 val instantiate_inducts : bool Config.T |
42 val is_locality_global : locality -> bool |
|
43 val fact_from_ref : |
42 val fact_from_ref : |
44 Proof.context -> unit Symtab.table -> thm list |
43 Proof.context -> unit Symtab.table -> thm list |
45 -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list |
44 -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list |
46 val all_facts : |
45 val all_facts : |
47 Proof.context -> 'a Symtab.table -> bool -> (term -> bool) -> thm list |
46 Proof.context -> 'a Symtab.table -> bool -> (term -> bool) -> thm list |
57 end; |
56 end; |
58 |
57 |
59 structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = |
58 structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = |
60 struct |
59 struct |
61 |
60 |
|
61 open ATP_Translate |
62 open Sledgehammer_Util |
62 open Sledgehammer_Util |
63 |
63 |
64 val trace = |
64 val trace = |
65 Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false) |
65 Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false) |
66 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
66 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
70 Attrib.setup_config_bool @{binding sledgehammer_new_monomorphizer} (K false) |
70 Attrib.setup_config_bool @{binding sledgehammer_new_monomorphizer} (K false) |
71 val ignore_no_atp = |
71 val ignore_no_atp = |
72 Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false) |
72 Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false) |
73 val instantiate_inducts = |
73 val instantiate_inducts = |
74 Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) |
74 Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) |
75 |
|
76 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained |
|
77 |
|
78 (* (quasi-)underapproximation of the truth *) |
|
79 fun is_locality_global Local = false |
|
80 | is_locality_global Assum = false |
|
81 | is_locality_global Chained = false |
|
82 | is_locality_global _ = true |
|
83 |
75 |
84 type relevance_fudge = |
76 type relevance_fudge = |
85 {local_const_multiplier : real, |
77 {local_const_multiplier : real, |
86 worse_irrel_freq : real, |
78 worse_irrel_freq : real, |
87 higher_order_irrel_weight : real, |
79 higher_order_irrel_weight : real, |