count number of iterations required for minimization (and fixed bug: minimization was always called)

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 14 12:25:02 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 14 19:30:48 2009 +0200
@@ -35,52 +35,72 @@
   posns: Position.T list
   }
 
+datatype min_data = MinData of {
+  calls: int,
+  ratios: int
+  }
 
 (* The first me_data component is only used if "minimize" is on.
    Then it records how metis behaves with un-minimized lemmas.
 *)
-datatype data = Data of sh_data * me_data * me_data
+datatype data = Data of sh_data * me_data * min_data * me_data
 
 fun make_sh_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) =
   ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa,
     time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}
 
+fun make_min_data (calls, ratios) =
+  MinData{calls=calls, ratios=ratios}
+
 fun make_me_data (calls, success, time, timeout, lemmas, posns) =
   MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
 
-val empty_data = Data(make_sh_data (0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0, 0, []),
-  make_me_data(0, 0, 0, 0, 0, []))
+val empty_data =
+  Data(make_sh_data (0, 0, 0, 0, 0),
+       make_me_data(0, 0, 0, 0, 0, []),
+       MinData{calls=0, ratios=0},
+       make_me_data(0, 0, 0, 0, 0, []))
 
 fun map_sh_data f
-  (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, meda)) =
+  (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) =
   Data (make_sh_data (f (calls, success, time_isa, time_atp, time_atp_fail)),
-        meda0, meda)
+        meda0, minda, meda)
 
-fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, meda)) =
-  Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), meda)
+fun map_min_data f
+  (Data(shda, meda0, MinData{calls,ratios}, meda)) =
+  Data(shda, meda0, make_min_data(f(calls,ratios)), meda)
 
-fun map_me_data f (Data (shda, meda0, MeData{calls,success,time,timeout,lemmas,posns})) =
-  Data(shda, meda0, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
+fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) =
+  Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda)
+
+fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,time,timeout,lemmas,posns})) =
+  Data(shda, meda0, minda, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
 
 val inc_sh_calls =
-  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-    => (sh_calls + 1, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail))
+  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
+    => (calls + 1, success, time_isa, time_atp, time_atp_fail))
 
 val inc_sh_success =
-  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-    => (sh_calls, sh_success + 1, sh_time_isa, sh_time_atp, sh_time_atp_fail))
+  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
+    => (calls, success + 1, time_isa, time_atp, time_atp_fail))
 
 fun inc_sh_time_isa t =
-  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-    => (sh_calls, sh_success, sh_time_isa + t, sh_time_atp, sh_time_atp_fail))
+  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
+    => (calls, success, time_isa + t, time_atp, time_atp_fail))
 
 fun inc_sh_time_atp t =
-  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-    => (sh_calls, sh_success, sh_time_isa, sh_time_atp + t, sh_time_atp_fail))
+  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
+    => (calls, success, time_isa, time_atp + t, time_atp_fail))
 
 fun inc_sh_time_atp_fail t =
-  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-    => (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail + t))
+  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
+    => (calls, success, time_isa, time_atp, time_atp_fail + t))
+
+val inc_min_calls =
+  map_min_data (fn (calls, ratios) => (calls + 1, ratios))
+
+fun inc_min_ratios n =
+  map_min_data (fn (calls, ratios) => (calls, ratios + n))
 
 val inc_metis_calls = map_me_data
  (fn (calls, success, time, timeout, lemmas,posns)
@@ -175,6 +195,12 @@
   then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns))
   else ()
  )
+
+fun log_min_data log calls ratios =
+  (log ("Number of minimizations: " ^ string_of_int calls);
+   log ("Minimization ratios: " ^ string_of_int ratios)
+  )
+
 in
 
 fun log_data id log (Data
@@ -182,7 +208,9 @@
       time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail},
     MeData{calls=metis_calls0,
       success=metis_success0, time=metis_time0, timeout=metis_timeout0,
-      lemmas=metis_lemmas0,posns=metis_posns0}, MeData{calls=metis_calls,
+      lemmas=metis_lemmas0,posns=metis_posns0},
+    MinData{calls=min_calls, ratios=min_ratios},
+    MeData{calls=metis_calls,
       success=metis_success, time=metis_time, timeout=metis_timeout,
       lemmas=metis_lemmas,posns=metis_posns})) =
   if sh_calls > 0
@@ -194,8 +222,9 @@
       metis_success metis_time metis_timeout metis_lemmas  metis_posns else ();
     log "";
     if metis_calls0 > 0
-      then log_metis_data log "unminimized " sh_calls sh_success metis_calls0
-              metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0
+      then (log_min_data log min_calls min_ratios; log "";
+            log_metis_data log "unminimized " sh_calls sh_success metis_calls0
+              metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
       else ()
    )
   else ()
@@ -305,6 +334,7 @@
 
 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
+    val n0 = length (these (!named_thms))
     val (prover_name, prover) = get_atp (Proof.theory_of st) args
     val minimize = AtpMinimal.minimalize prover prover_name
     val timeout =
@@ -313,14 +343,16 @@
       |> the_default 5
     val _ = log separator
   in
-    (case minimize timeout st (these (!named_thms)) of
-      (SOME named_thms', msg) =>
-        if length named_thms' = length (these (!named_thms))
-        then log (minimize_tag id ^ "already minimal")
-        else
-         (named_thms := SOME named_thms';
-          log (minimize_tag id ^ "succeeded:\n" ^ msg))
-    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg))
+    case minimize timeout st (these (!named_thms)) of
+      (SOME (named_thms',its), msg) =>
+        (change_data id inc_min_calls;
+         change_data id (inc_min_ratios ((100*its) div n0));
+         if length named_thms' = n0
+         then log (minimize_tag id ^ "already minimal")
+         else (named_thms := SOME named_thms';
+               log (minimize_tag id ^ "succeeded:\n" ^ msg))
+        )
+    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
   end
 
 
@@ -364,9 +396,8 @@
     val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
     val _ = if_enabled minimizeK
       (Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))))
-    val _ = if is_some (!named_thms)
-      then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st
-      else ()
+    val _ = if_enabled minimizeK
+      (Mirabelle.catch minimize_tag (run_minimize args named_thms))
     val _ = if is_some (!named_thms)
       then Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st
       else ()

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Sep 14 12:25:02 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Sep 14 19:30:48 2009 +0200
@@ -7,7 +7,7 @@
 signature ATP_MINIMAL =
 sig
   val minimalize: AtpManager.prover -> string -> int -> Proof.state ->
-    (string * thm list) list -> (string * thm list) list option * string
+    (string * thm list) list -> ((string * thm list) list * int) option * string
 end
 
 structure AtpMinimal: ATP_MINIMAL =
@@ -69,9 +69,14 @@
          forall e in v. ~p(v \ e)
    *)
   fun minimal p s =
-    case min p [] s of
-      [x] => if p [] then [] else [x]
-    | m => m
+    let val c = ref 0
+        fun pc xs = (c := !c + 1; p xs)
+    in
+    (case min pc [] s of
+       [x] => if pc [] then [] else [x]
+     | m => m,
+     !c)
+    end
 end
 
 
@@ -150,13 +155,14 @@
               filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
             else
               name_thms_pairs
-          val min_thms = if null to_use then []
+          val (min_thms, n) = if null to_use then ([], 0)
             else minimal (test_thms (SOME filtered)) to_use
           val min_names = order_unique (map fst min_thms)
+          val _ = println ("Interations: " ^ string_of_int n)
           val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
           val _ = debug_fn (fn () => print_names min_thms)
         in
-          answer' (SOME min_thms) ("Try this command: " ^
+          answer' (SOME(min_thms,n)) ("Try this command: " ^
             Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
         end
     | (Timeout, _) =>
@@ -167,7 +173,7 @@
     | (Failure, _) =>
         answer'' "Failure: No proof with the theorems supplied")
     handle ResHolClause.TOO_TRIVIAL =>
-        answer' (SOME []) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+        answer' (SOME ([],0)) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
     | ERROR msg =>
         answer'' ("Error: " ^ msg)
   end