author | blanchet |
Mon, 30 Aug 2010 12:44:00 +0200 | |
changeset 38900 | 853a061af37d |
parent 38897 | 92ca38d18af0 |
child 38902 | c91be1e503bd |
permissions | -rw-r--r-- |
38892 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML |
2 |
Author: Jasmin Blanchette, TU Munich |
|
3 |
*) |
|
4 |
||
5 |
structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = |
|
6 |
struct |
|
7 |
||
8 |
structure Prooftab = |
|
9 |
Table(type key = int * int val ord = prod_ord int_ord int_ord); |
|
10 |
||
11 |
val proof_table = Unsynchronized.ref Prooftab.empty |
|
12 |
||
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
13 |
val num_successes = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
14 |
val num_failures = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
15 |
val num_found_proofs = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
16 |
val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
17 |
val num_found_facts = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
18 |
val num_lost_facts = Unsynchronized.ref ([] : (int * int) list) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
19 |
|
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
20 |
fun get id c = the_default 0 (AList.lookup (op =) (!c) id) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
21 |
fun add id c n = |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
22 |
c := (case AList.lookup (op =) (!c) id of |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
23 |
SOME m => AList.update (op =) (id, m + n) (!c) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
24 |
| NONE => (id, n) :: !c) |
38894 | 25 |
|
26 |
fun init proof_file _ thy = |
|
38892 | 27 |
let |
28 |
fun do_line line = |
|
29 |
case line |> space_explode ":" of |
|
30 |
[line_num, col_num, proof] => |
|
31 |
SOME (pairself (the o Int.fromString) (line_num, col_num), |
|
32 |
proof |> space_explode " " |> filter_out (curry (op =) "")) |
|
33 |
| _ => NONE |
|
38894 | 34 |
val proofs = File.read (Path.explode proof_file) |
38892 | 35 |
val proof_tab = |
36 |
proofs |> space_explode "\n" |
|
37 |
|> map_filter do_line |
|
38 |
|> AList.coalesce (op =) |
|
39 |
|> Prooftab.make |
|
40 |
in proof_table := proof_tab; thy end |
|
41 |
||
38894 | 42 |
fun percentage a b = if b = 0 then "N/A" else string_of_int (a * 100 div b) |
43 |
fun percentage_alt a b = percentage a (a + b) |
|
44 |
||
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
45 |
fun done id ({log, ...} : Mirabelle.done_args) = |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
46 |
if get id num_successes + get id num_failures > 0 then |
38897 | 47 |
(log ""; |
48 |
log ("Number of overall successes: " ^ |
|
49 |
string_of_int (get id num_successes)); |
|
50 |
log ("Number of overall failures: " ^ string_of_int (get id num_failures)); |
|
38894 | 51 |
log ("Overall success rate: " ^ |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
52 |
percentage_alt (get id num_successes) (get id num_failures) ^ "%"); |
38897 | 53 |
log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs)); |
54 |
log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs)); |
|
38894 | 55 |
log ("Proof found rate: " ^ |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
56 |
percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^ |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
57 |
"%"); |
38897 | 58 |
log ("Number of found facts: " ^ string_of_int (get id num_found_facts)); |
59 |
log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts)); |
|
38894 | 60 |
log ("Fact found rate: " ^ |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
61 |
percentage_alt (get id num_found_facts) (get id num_lost_facts) ^ |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
62 |
"%")) |
38894 | 63 |
else |
64 |
() |
|
38892 | 65 |
|
66 |
val default_max_relevant = 300 |
|
67 |
||
38897 | 68 |
fun with_index (i, s) = s ^ "@" ^ string_of_int i |
69 |
||
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
70 |
fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) = |
38892 | 71 |
case (Position.line_of pos, Position.column_of pos) of |
72 |
(SOME line_num, SOME col_num) => |
|
73 |
(case Prooftab.lookup (!proof_table) (line_num, col_num) of |
|
74 |
SOME proofs => |
|
75 |
let |
|
76 |
val {context = ctxt, facts, goal} = Proof.goal pre |
|
77 |
val thy = ProofContext.theory_of ctxt |
|
78 |
val {relevance_thresholds, full_types, max_relevant, theory_relevant, |
|
79 |
...} = Sledgehammer_Isar.default_params thy args |
|
80 |
val subgoal = 1 |
|
81 |
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal |
|
82 |
val facts = |
|
83 |
Sledgehammer_Fact_Filter.relevant_facts ctxt full_types |
|
84 |
relevance_thresholds |
|
85 |
(the_default default_max_relevant max_relevant) |
|
86 |
(the_default false theory_relevant) |
|
87 |
{add = [], del = [], only = false} facts hyp_ts concl_t |
|
88 |
|> map (fst o fst) |
|
38894 | 89 |
val (found_facts, lost_facts) = |
38892 | 90 |
List.concat proofs |> sort_distinct string_ord |
38897 | 91 |
|> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |
92 |
|> List.partition (curry (op <=) 0 o fst) |
|
93 |
|>> sort (prod_ord int_ord string_ord) ||> map snd |
|
38892 | 94 |
val found_proofs = filter (forall (member (op =) facts)) proofs |
38894 | 95 |
val n = length found_proofs |
38892 | 96 |
val _ = |
38894 | 97 |
if n = 0 then |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
98 |
(add id num_failures 1; log "Failure") |
38894 | 99 |
else |
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
100 |
(add id num_successes 1; |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
101 |
add id num_found_proofs n; |
38897 | 102 |
log ("Success (" ^ string_of_int n ^ " of " ^ |
103 |
string_of_int (length proofs) ^ " proofs)")) |
|
38896
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
104 |
val _ = add id num_lost_proofs (length proofs - n) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
105 |
val _ = add id num_found_facts (length found_facts) |
b36ab8860748
allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
blanchet
parents:
38894
diff
changeset
|
106 |
val _ = add id num_lost_facts (length lost_facts) |
38897 | 107 |
val _ = if null found_facts then |
108 |
() |
|
109 |
else |
|
110 |
log ("Found facts: " ^ commas (map with_index found_facts)) |
|
38894 | 111 |
val _ = if null lost_facts then () |
112 |
else log ("Lost facts: " ^ commas lost_facts) |
|
38892 | 113 |
in () end |
38894 | 114 |
| NONE => log "No known proof") |
38892 | 115 |
| _ => () |
116 |
||
38894 | 117 |
val proof_fileK = "proof_file" |
118 |
||
38900
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
119 |
val relevance_filter_args = |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
120 |
[("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight), |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
121 |
("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight), |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
122 |
("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight), |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
123 |
("theory_bonus", Sledgehammer_Fact_Filter.theory_bonus), |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
124 |
("local_bonus", Sledgehammer_Fact_Filter.local_bonus), |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
125 |
("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus), |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
126 |
("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor), |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
127 |
("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold), |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
128 |
("max_max_imperfect_fudge_factor", |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
129 |
Sledgehammer_Fact_Filter.max_max_imperfect_fudge_factor)] |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
130 |
|
38894 | 131 |
fun invoke args = |
132 |
let |
|
133 |
val (pf_args, other_args) = |
|
134 |
args |> List.partition (curry (op =) proof_fileK o fst) |
|
38900
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
135 |
||> filter (fn (key, value) => |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
136 |
case AList.lookup (op =) relevance_filter_args key of |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
137 |
SOME rf => (rf := the (Real.fromString value); false) |
853a061af37d
allow configuration of fact filter fudge factors
blanchet
parents:
38897
diff
changeset
|
138 |
| NONE => true) |
38894 | 139 |
val proof_file = case pf_args of |
140 |
[] => error "No \"proof_file\" specified" |
|
141 |
| (_, s) :: _ => s |
|
142 |
in Mirabelle.register (init proof_file, action other_args, done) end |
|
38892 | 143 |
|
144 |
end; |
|
38894 | 145 |
|
146 |
(* Workaround to keep the "mirabelle.pl" script happy *) |
|
147 |
structure Mirabelle_Sledgehammer_filter = Mirabelle_Sledgehammer_Filter; |