# HG changeset patch
# User blanchet
# Date 1283159470 -7200
# Node ID e85263e281bebc7e765de6ed741a078c3611d5cb
# Parent  aa21c33a104fb49b1216320588f194e4b9378892
improve new "sledgehammer_filter" action

diff -r aa21c33a104f -r e85263e281be src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Aug 30 11:10:44 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Aug 30 11:11:10 2010 +0200
@@ -10,7 +10,14 @@
 
 val proof_table = Unsynchronized.ref Prooftab.empty
 
-fun init id thy =
+val num_successes = Unsynchronized.ref 0
+val num_failures = Unsynchronized.ref 0
+val num_found_proofs = Unsynchronized.ref 0
+val num_lost_proofs = Unsynchronized.ref 0
+val num_found_facts = Unsynchronized.ref 0
+val num_lost_facts = Unsynchronized.ref 0
+
+fun init proof_file _ thy =
   let
     fun do_line line =
       case line |> space_explode ":" of
@@ -18,7 +25,7 @@
         SOME (pairself (the o Int.fromString) (line_num, col_num),
               proof |> space_explode " " |> filter_out (curry (op =) ""))
        | _ => NONE
-    val proofs = File.read (Path.explode "$HOME/Judgement/AllProofs/NS_Shared.txt")
+    val proofs = File.read (Path.explode proof_file)
     val proof_tab =
       proofs |> space_explode "\n"
              |> map_filter do_line
@@ -26,11 +33,29 @@
              |> Prooftab.make
   in proof_table := proof_tab; thy end
 
-fun done id (args : Mirabelle.done_args) = ()
+fun percentage a b = if b = 0 then "N/A" else string_of_int (a * 100 div b)
+fun percentage_alt a b = percentage a (a + b)
+
+fun done _ ({log, ...} : Mirabelle.done_args) =
+  if !num_successes + !num_failures > 0 then
+    (log ("Number of overall success: " ^ Int.toString (!num_successes));
+     log ("Number of overall failures: " ^ Int.toString (!num_failures));
+     log ("Overall success rate: " ^
+          percentage_alt (!num_successes) (!num_failures) ^ "%");
+     log ("Number of found proofs: " ^ Int.toString (!num_found_proofs));
+     log ("Number of lost proofs: " ^ Int.toString (!num_lost_proofs));
+     log ("Proof found rate: " ^
+          percentage_alt (!num_found_proofs) (!num_lost_proofs) ^ "%");
+     log ("Number of found facts: " ^ Int.toString (!num_found_facts));
+     log ("Number of lost facts: " ^ Int.toString (!num_lost_facts));
+     log ("Fact found rate: " ^
+          percentage_alt (!num_found_facts) (!num_lost_facts) ^ "%"))
+  else
+    ()
 
 val default_max_relevant = 300
 
-fun action args id ({pre, pos, ...} : Mirabelle.run_args) =
+fun action args _ ({pre, pos, log, ...} : Mirabelle.run_args) =
   case (Position.line_of pos, Position.column_of pos) of
     (SOME line_num, SOME col_num) =>
     (case Prooftab.lookup (!proof_table) (line_num, col_num) of
@@ -49,21 +74,42 @@
                (the_default false theory_relevant)
                {add = [], del = [], only = false} facts hyp_ts concl_t
            |> map (fst o fst)
-         val (found_facts, missing_facts) =
+         val (found_facts, lost_facts) =
            List.concat proofs |> sort_distinct string_ord
            |> List.partition (member (op =) facts)
          val found_proofs = filter (forall (member (op =) facts)) proofs
+         val n = length found_proofs
          val _ =
-           case length found_proofs of
-             0 => writeln "Failure"
-           | n => writeln ("Success (" ^ Int.toString n ^ " of " ^
-                           Int.toString (length proofs) ^ " proofs)")
-         val _ = writeln ("Found facts: " ^ commas found_facts)
-         val _ = writeln ("Missing facts: " ^ commas missing_facts)
+           if n = 0 then
+             (num_failures := !num_failures + 1; log "Failure")
+           else
+             (num_successes := !num_successes + 1;
+              num_found_proofs := !num_found_proofs + n;
+              log ("Success (" ^ Int.toString n ^ " of " ^
+                   Int.toString (length proofs) ^ " proofs)"))
+         val _ = num_lost_proofs := !num_lost_proofs + length proofs - n
+         val _ = num_found_facts := !num_found_facts + (length found_facts)
+         val _ = num_lost_facts := !num_lost_facts + (length lost_facts)
+         val _ = if null found_facts then ()
+                 else log ("Found facts: " ^ commas found_facts)
+         val _ = if null lost_facts then ()
+                 else log ("Lost facts: " ^ commas lost_facts)
        in () end
-     | NONE => ())
+     | NONE => log "No known proof")
   | _ => ()
 
-fun invoke args = Mirabelle.register (init, action args, done)
+val proof_fileK = "proof_file"
+
+fun invoke args =
+  let
+    val (pf_args, other_args) =
+      args |> List.partition (curry (op =) proof_fileK o fst)
+    val proof_file = case pf_args of
+                       [] => error "No \"proof_file\" specified"
+                     | (_, s) :: _ => s
+  in Mirabelle.register (init proof_file, action other_args, done) end
 
 end;
+
+(* Workaround to keep the "mirabelle.pl" script happy *)
+structure Mirabelle_Sledgehammer_filter = Mirabelle_Sledgehammer_Filter;