8 structure Prooftab = |
8 structure Prooftab = |
9 Table(type key = int * int val ord = prod_ord int_ord int_ord); |
9 Table(type key = int * int val ord = prod_ord int_ord int_ord); |
10 |
10 |
11 val proof_table = Unsynchronized.ref Prooftab.empty |
11 val proof_table = Unsynchronized.ref Prooftab.empty |
12 |
12 |
13 fun init id thy = |
13 val num_successes = Unsynchronized.ref 0 |
|
14 val num_failures = Unsynchronized.ref 0 |
|
15 val num_found_proofs = Unsynchronized.ref 0 |
|
16 val num_lost_proofs = Unsynchronized.ref 0 |
|
17 val num_found_facts = Unsynchronized.ref 0 |
|
18 val num_lost_facts = Unsynchronized.ref 0 |
|
19 |
|
20 fun init proof_file _ thy = |
14 let |
21 let |
15 fun do_line line = |
22 fun do_line line = |
16 case line |> space_explode ":" of |
23 case line |> space_explode ":" of |
17 [line_num, col_num, proof] => |
24 [line_num, col_num, proof] => |
18 SOME (pairself (the o Int.fromString) (line_num, col_num), |
25 SOME (pairself (the o Int.fromString) (line_num, col_num), |
19 proof |> space_explode " " |> filter_out (curry (op =) "")) |
26 proof |> space_explode " " |> filter_out (curry (op =) "")) |
20 | _ => NONE |
27 | _ => NONE |
21 val proofs = File.read (Path.explode "$HOME/Judgement/AllProofs/NS_Shared.txt") |
28 val proofs = File.read (Path.explode proof_file) |
22 val proof_tab = |
29 val proof_tab = |
23 proofs |> space_explode "\n" |
30 proofs |> space_explode "\n" |
24 |> map_filter do_line |
31 |> map_filter do_line |
25 |> AList.coalesce (op =) |
32 |> AList.coalesce (op =) |
26 |> Prooftab.make |
33 |> Prooftab.make |
27 in proof_table := proof_tab; thy end |
34 in proof_table := proof_tab; thy end |
28 |
35 |
29 fun done id (args : Mirabelle.done_args) = () |
36 fun percentage a b = if b = 0 then "N/A" else string_of_int (a * 100 div b) |
|
37 fun percentage_alt a b = percentage a (a + b) |
|
38 |
|
39 fun done _ ({log, ...} : Mirabelle.done_args) = |
|
40 if !num_successes + !num_failures > 0 then |
|
41 (log ("Number of overall success: " ^ Int.toString (!num_successes)); |
|
42 log ("Number of overall failures: " ^ Int.toString (!num_failures)); |
|
43 log ("Overall success rate: " ^ |
|
44 percentage_alt (!num_successes) (!num_failures) ^ "%"); |
|
45 log ("Number of found proofs: " ^ Int.toString (!num_found_proofs)); |
|
46 log ("Number of lost proofs: " ^ Int.toString (!num_lost_proofs)); |
|
47 log ("Proof found rate: " ^ |
|
48 percentage_alt (!num_found_proofs) (!num_lost_proofs) ^ "%"); |
|
49 log ("Number of found facts: " ^ Int.toString (!num_found_facts)); |
|
50 log ("Number of lost facts: " ^ Int.toString (!num_lost_facts)); |
|
51 log ("Fact found rate: " ^ |
|
52 percentage_alt (!num_found_facts) (!num_lost_facts) ^ "%")) |
|
53 else |
|
54 () |
30 |
55 |
31 val default_max_relevant = 300 |
56 val default_max_relevant = 300 |
32 |
57 |
33 fun action args id ({pre, pos, ...} : Mirabelle.run_args) = |
58 fun action args _ ({pre, pos, log, ...} : Mirabelle.run_args) = |
34 case (Position.line_of pos, Position.column_of pos) of |
59 case (Position.line_of pos, Position.column_of pos) of |
35 (SOME line_num, SOME col_num) => |
60 (SOME line_num, SOME col_num) => |
36 (case Prooftab.lookup (!proof_table) (line_num, col_num) of |
61 (case Prooftab.lookup (!proof_table) (line_num, col_num) of |
37 SOME proofs => |
62 SOME proofs => |
38 let |
63 let |
47 relevance_thresholds |
72 relevance_thresholds |
48 (the_default default_max_relevant max_relevant) |
73 (the_default default_max_relevant max_relevant) |
49 (the_default false theory_relevant) |
74 (the_default false theory_relevant) |
50 {add = [], del = [], only = false} facts hyp_ts concl_t |
75 {add = [], del = [], only = false} facts hyp_ts concl_t |
51 |> map (fst o fst) |
76 |> map (fst o fst) |
52 val (found_facts, missing_facts) = |
77 val (found_facts, lost_facts) = |
53 List.concat proofs |> sort_distinct string_ord |
78 List.concat proofs |> sort_distinct string_ord |
54 |> List.partition (member (op =) facts) |
79 |> List.partition (member (op =) facts) |
55 val found_proofs = filter (forall (member (op =) facts)) proofs |
80 val found_proofs = filter (forall (member (op =) facts)) proofs |
|
81 val n = length found_proofs |
56 val _ = |
82 val _ = |
57 case length found_proofs of |
83 if n = 0 then |
58 0 => writeln "Failure" |
84 (num_failures := !num_failures + 1; log "Failure") |
59 | n => writeln ("Success (" ^ Int.toString n ^ " of " ^ |
85 else |
60 Int.toString (length proofs) ^ " proofs)") |
86 (num_successes := !num_successes + 1; |
61 val _ = writeln ("Found facts: " ^ commas found_facts) |
87 num_found_proofs := !num_found_proofs + n; |
62 val _ = writeln ("Missing facts: " ^ commas missing_facts) |
88 log ("Success (" ^ Int.toString n ^ " of " ^ |
|
89 Int.toString (length proofs) ^ " proofs)")) |
|
90 val _ = num_lost_proofs := !num_lost_proofs + length proofs - n |
|
91 val _ = num_found_facts := !num_found_facts + (length found_facts) |
|
92 val _ = num_lost_facts := !num_lost_facts + (length lost_facts) |
|
93 val _ = if null found_facts then () |
|
94 else log ("Found facts: " ^ commas found_facts) |
|
95 val _ = if null lost_facts then () |
|
96 else log ("Lost facts: " ^ commas lost_facts) |
63 in () end |
97 in () end |
64 | NONE => ()) |
98 | NONE => log "No known proof") |
65 | _ => () |
99 | _ => () |
66 |
100 |
67 fun invoke args = Mirabelle.register (init, action args, done) |
101 val proof_fileK = "proof_file" |
|
102 |
|
103 fun invoke args = |
|
104 let |
|
105 val (pf_args, other_args) = |
|
106 args |> List.partition (curry (op =) proof_fileK o fst) |
|
107 val proof_file = case pf_args of |
|
108 [] => error "No \"proof_file\" specified" |
|
109 | (_, s) :: _ => s |
|
110 in Mirabelle.register (init proof_file, action other_args, done) end |
68 |
111 |
69 end; |
112 end; |
|
113 |
|
114 (* Workaround to keep the "mirabelle.pl" script happy *) |
|
115 structure Mirabelle_Sledgehammer_filter = Mirabelle_Sledgehammer_Filter; |