merged

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 24 15:00:17 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 24 17:26:05 2009 +0200
@@ -16,7 +16,7 @@
   type done_args = {last: Toplevel.state, log: string -> unit}
   type done_action = int -> done_args -> unit
   type run_args = {pre: Proof.state, post: Toplevel.state option,
-    timeout: Time.time, log: string -> unit, pos: Position.T}
+    timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
   type run_action = int -> run_args -> unit
   type action = init_action * run_action * done_action
   val catch : (int -> string) -> run_action -> run_action
@@ -56,7 +56,7 @@
 type done_args = {last: Toplevel.state, log: string -> unit}
 type done_action = int -> done_args -> unit
 type run_args = {pre: Proof.state, post: Toplevel.state option,
-  timeout: Time.time, log: string -> unit, pos: Position.T}
+  timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
 type run_action = int -> run_args -> unit
 type action = init_action * run_action * done_action
 
@@ -95,9 +95,9 @@
 
 fun log_sep thy = log thy "------------------"
 
-fun apply_actions thy pos info (pre, post, time) actions =
+fun apply_actions thy pos name info (pre, post, time) actions =
   let
-    fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos}
+    fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name}
     fun run (id, run, _) = (apply (run id); log_sep thy)
   in (log thy info; log_sep thy; List.app run actions) end
 
@@ -121,7 +121,7 @@
     val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
     val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
   in
-    only_within_range thy pos (apply_actions thy pos info st) (Actions.get thy)
+    only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy)
   end
 
 fun done_actions st =

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 24 15:00:17 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 24 17:26:05 2009 +0200
@@ -31,6 +31,7 @@
 datatype me_data = MeData of {
   calls: int,
   success: int,
+  proofs: int,
   time: int,
   timeout: int,
   lemmas: int,
@@ -55,14 +56,14 @@
 fun make_min_data (succs, ab_ratios, it_ratios) =
   MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
 
-fun make_me_data (calls, success, time, timeout, lemmas, posns) =
-  MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
+fun make_me_data (calls, success, proofs, time, timeout, lemmas, posns) =
+  MeData{calls=calls, success=success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
 
 val empty_data =
   Data(make_sh_data (0, 0, 0, 0, 0, 0),
-       make_me_data(0, 0, 0, 0, 0, []),
+       make_me_data(0, 0, 0, 0, 0, 0, []),
        MinData{succs=0, ab_ratios=0, it_ratios=0},
-       make_me_data(0, 0, 0, 0, 0, []))
+       make_me_data(0, 0, 0, 0, 0, 0, []))
 
 fun map_sh_data f
   (Data (ShData{calls, success, lemmas, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) =
@@ -73,11 +74,11 @@
   (Data(shda, meda0, MinData{succs,ab_ratios,it_ratios}, meda)) =
   Data(shda, meda0, make_min_data(f(succs,ab_ratios,it_ratios)), meda)
 
-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_data0 f (Data (shda, MeData{calls,success,proofs,time,timeout,lemmas,posns}, minda, meda)) =
+  Data(shda, make_me_data(f (calls,success,proofs,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)))
+fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,proofs,time,timeout,lemmas,posns})) =
+  Data(shda, meda0, minda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,posns)))
 
 val inc_sh_calls =
   map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
@@ -113,52 +114,60 @@
   map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
 
 val inc_metis_calls = map_me_data
- (fn (calls, success, time, timeout, lemmas,posns)
-  => (calls + 1, success, time, timeout, lemmas,posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls + 1, success, proofs, time, timeout, lemmas,posns))
 
 val inc_metis_success = map_me_data
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success + 1, time, timeout, lemmas,posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success + 1, proofs, time, timeout, lemmas,posns))
+
+val inc_metis_proofs = map_me_data
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs + 1, time, timeout, lemmas,posns))
 
 fun inc_metis_time t = map_me_data
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success, time + t, timeout, lemmas,posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs, time + t, timeout, lemmas,posns))
 
 val inc_metis_timeout = map_me_data
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success, time, timeout + 1, lemmas,posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs, time, timeout + 1, lemmas,posns))
 
 fun inc_metis_lemmas n = map_me_data
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success, time, timeout, lemmas + n, posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs, time, timeout, lemmas + n, posns))
 
 fun inc_metis_posns pos = map_me_data
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success, time, timeout, lemmas, pos::posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs, time, timeout, lemmas, pos::posns))
 
 val inc_metis_calls0 = map_me_data0 
-(fn (calls, success, time, timeout, lemmas,posns)
-  => (calls + 1, success, time, timeout, lemmas,posns))
+(fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls + 1, success, proofs, time, timeout, lemmas,posns))
 
 val inc_metis_success0 = map_me_data0
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success + 1, time, timeout, lemmas,posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success + 1, proofs, time, timeout, lemmas,posns))
+
+val inc_metis_proofs0 = map_me_data0
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs + 1, time, timeout, lemmas,posns))
 
 fun inc_metis_time0 t = map_me_data0
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success, time + t, timeout, lemmas,posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs, time + t, timeout, lemmas,posns))
 
 val inc_metis_timeout0 = map_me_data0
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success, time, timeout + 1, lemmas,posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs, time, timeout + 1, lemmas,posns))
 
 fun inc_metis_lemmas0 n = map_me_data0
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success, time, timeout, lemmas + n, posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs, time, timeout, lemmas + n, posns))
 
 fun inc_metis_posns0 pos = map_me_data0
- (fn (calls,success,time,timeout,lemmas,posns)
-  => (calls, success, time, timeout, lemmas, pos::posns))
+ (fn (calls,success,proofs,time,timeout,lemmas,posns)
+  => (calls, success, proofs, time, timeout, lemmas, pos::posns))
 
 local
 
@@ -190,10 +199,10 @@
   let val str0 = string_of_int o the_default 0
   in str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) end
 
-fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_time
+fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_proofs metis_time
     metis_timeout metis_lemmas metis_posns =
  (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
-  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success);
+  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^ " (proof: " ^ str metis_proofs ^ ")");
   log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
   log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
   log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
@@ -216,11 +225,11 @@
 fun log_data id log (Data
    (ShData{calls=sh_calls, lemmas=sh_lemmas, success=sh_success,
       time_isa=sh_time_isa,time_atp=sh_time_atp,time_atp_fail=sh_time_atp_fail},
-    MeData{calls=metis_calls0,
+    MeData{calls=metis_calls0, proofs=metis_proofs0,
       success=metis_success0, time=metis_time0, timeout=metis_timeout0,
       lemmas=metis_lemmas0,posns=metis_posns0},
     MinData{succs=min_succs, ab_ratios=ab_ratios, it_ratios=it_ratios},
-    MeData{calls=metis_calls,
+    MeData{calls=metis_calls, proofs=metis_proofs,
       success=metis_success, time=metis_time, timeout=metis_timeout,
       lemmas=metis_lemmas,posns=metis_posns})) =
   if sh_calls > 0
@@ -229,12 +238,12 @@
     log_sh_data log sh_calls sh_success sh_lemmas sh_time_isa sh_time_atp sh_time_atp_fail;
     log "";
     if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls
-      metis_success metis_time metis_timeout metis_lemmas  metis_posns else ();
+      metis_success metis_proofs metis_time metis_timeout metis_lemmas  metis_posns else ();
     log "";
     if metis_calls0 > 0
       then (log_min_data log min_succs ab_ratios it_ratios; log "";
             log_metis_data log "unminimized " sh_calls sh_success metis_calls0
-              metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
+              metis_success0 metis_proofs0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
       else ()
    )
   else ()
@@ -376,8 +385,8 @@
   end
 
 
-fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout,
-    inc_metis_lemmas, inc_metis_posns) args named_thms id
+fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time, inc_metis_timeout,
+    inc_metis_lemmas, inc_metis_posns) args name named_thms id
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
     fun metis thms ctxt = MetisTools.metis_tac ctxt thms
@@ -388,6 +397,7 @@
           change_data id (inc_metis_lemmas (length named_thms));
           change_data id (inc_metis_time t);
           change_data id (inc_metis_posns pos);
+          if name = "proof" then change_data id inc_metis_proofs else ();
           "succeeded (" ^ string_of_int t ^ ")")
     fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
       handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
@@ -401,13 +411,13 @@
     |> log o prefix (metis_tag id) 
   end
 
-fun sledgehammer_action args id (st as {log, pre, ...}: Mirabelle.run_args) =
+fun sledgehammer_action args id (st as {log, pre, name, ...}: Mirabelle.run_args) =
   if can Logic.dest_conjunction (Thm.major_prem_of(snd(snd(Proof.get_goal pre))))
   then () else
   let
-    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
+    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time,
         inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
-    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0,
+    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_proofs0, inc_metis_time0,
         inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
     val named_thms = ref (NONE : (string * thm list) list option)
     val minimize = AList.defined (op =) args minimizeK
@@ -416,12 +426,12 @@
     if is_some (!named_thms)
       then
        (if minimize
-          then Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))) id st
+          then Mirabelle.catch metis_tag (run_metis metis0_fns args name (these (!named_thms))) id st
           else ();
        if minimize andalso not(null(these(!named_thms)))
          then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st
          else ();
-       Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st)
+       Mirabelle.catch metis_tag (run_metis metis_fns args name (these (!named_thms))) id st)
     else ()
   end