record how many "proof"s are solved by s/h
authornipkow
Thu Sep 24 17:25:42 2009 +0200 (2009-09-24)
changeset 32676b1c85a117dec
parent 32639 a6909ef949aa
child 32677 8854e892cf3e
record how many "proof"s are solved by s/h
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Sep 21 16:16:16 2009 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 24 17:25:42 2009 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    type done_args = {last: Toplevel.state, log: string -> unit}
     1.5    type done_action = int -> done_args -> unit
     1.6    type run_args = {pre: Proof.state, post: Toplevel.state option,
     1.7 -    timeout: Time.time, log: string -> unit, pos: Position.T}
     1.8 +    timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
     1.9    type run_action = int -> run_args -> unit
    1.10    type action = init_action * run_action * done_action
    1.11    val catch : (int -> string) -> run_action -> run_action
    1.12 @@ -56,7 +56,7 @@
    1.13  type done_args = {last: Toplevel.state, log: string -> unit}
    1.14  type done_action = int -> done_args -> unit
    1.15  type run_args = {pre: Proof.state, post: Toplevel.state option,
    1.16 -  timeout: Time.time, log: string -> unit, pos: Position.T}
    1.17 +  timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
    1.18  type run_action = int -> run_args -> unit
    1.19  type action = init_action * run_action * done_action
    1.20  
    1.21 @@ -95,9 +95,9 @@
    1.22  
    1.23  fun log_sep thy = log thy "------------------"
    1.24  
    1.25 -fun apply_actions thy pos info (pre, post, time) actions =
    1.26 +fun apply_actions thy pos name info (pre, post, time) actions =
    1.27    let
    1.28 -    fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos}
    1.29 +    fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name}
    1.30      fun run (id, run, _) = (apply (run id); log_sep thy)
    1.31    in (log thy info; log_sep thy; List.app run actions) end
    1.32  
    1.33 @@ -121,7 +121,7 @@
    1.34      val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
    1.35      val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
    1.36    in
    1.37 -    only_within_range thy pos (apply_actions thy pos info st) (Actions.get thy)
    1.38 +    only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy)
    1.39    end
    1.40  
    1.41  fun done_actions st =
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 21 16:16:16 2009 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 24 17:25:42 2009 +0200
     2.3 @@ -31,6 +31,7 @@
     2.4  datatype me_data = MeData of {
     2.5    calls: int,
     2.6    success: int,
     2.7 +  proofs: int,
     2.8    time: int,
     2.9    timeout: int,
    2.10    lemmas: int,
    2.11 @@ -55,14 +56,14 @@
    2.12  fun make_min_data (succs, ab_ratios, it_ratios) =
    2.13    MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
    2.14  
    2.15 -fun make_me_data (calls, success, time, timeout, lemmas, posns) =
    2.16 -  MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
    2.17 +fun make_me_data (calls, success, proofs, time, timeout, lemmas, posns) =
    2.18 +  MeData{calls=calls, success=success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
    2.19  
    2.20  val empty_data =
    2.21    Data(make_sh_data (0, 0, 0, 0, 0, 0),
    2.22 -       make_me_data(0, 0, 0, 0, 0, []),
    2.23 +       make_me_data(0, 0, 0, 0, 0, 0, []),
    2.24         MinData{succs=0, ab_ratios=0, it_ratios=0},
    2.25 -       make_me_data(0, 0, 0, 0, 0, []))
    2.26 +       make_me_data(0, 0, 0, 0, 0, 0, []))
    2.27  
    2.28  fun map_sh_data f
    2.29    (Data (ShData{calls, success, lemmas, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) =
    2.30 @@ -73,11 +74,11 @@
    2.31    (Data(shda, meda0, MinData{succs,ab_ratios,it_ratios}, meda)) =
    2.32    Data(shda, meda0, make_min_data(f(succs,ab_ratios,it_ratios)), meda)
    2.33  
    2.34 -fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) =
    2.35 -  Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda)
    2.36 +fun map_me_data0 f (Data (shda, MeData{calls,success,proofs,time,timeout,lemmas,posns}, minda, meda)) =
    2.37 +  Data(shda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,posns)), minda, meda)
    2.38  
    2.39 -fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,time,timeout,lemmas,posns})) =
    2.40 -  Data(shda, meda0, minda, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
    2.41 +fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,proofs,time,timeout,lemmas,posns})) =
    2.42 +  Data(shda, meda0, minda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,posns)))
    2.43  
    2.44  val inc_sh_calls =
    2.45    map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
    2.46 @@ -113,52 +114,60 @@
    2.47    map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
    2.48  
    2.49  val inc_metis_calls = map_me_data
    2.50 - (fn (calls, success, time, timeout, lemmas,posns)
    2.51 -  => (calls + 1, success, time, timeout, lemmas,posns))
    2.52 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.53 +  => (calls + 1, success, proofs, time, timeout, lemmas,posns))
    2.54  
    2.55  val inc_metis_success = map_me_data
    2.56 - (fn (calls,success,time,timeout,lemmas,posns)
    2.57 -  => (calls, success + 1, time, timeout, lemmas,posns))
    2.58 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.59 +  => (calls, success + 1, proofs, time, timeout, lemmas,posns))
    2.60 +
    2.61 +val inc_metis_proofs = map_me_data
    2.62 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.63 +  => (calls, success, proofs + 1, time, timeout, lemmas,posns))
    2.64  
    2.65  fun inc_metis_time t = map_me_data
    2.66 - (fn (calls,success,time,timeout,lemmas,posns)
    2.67 -  => (calls, success, time + t, timeout, lemmas,posns))
    2.68 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.69 +  => (calls, success, proofs, time + t, timeout, lemmas,posns))
    2.70  
    2.71  val inc_metis_timeout = map_me_data
    2.72 - (fn (calls,success,time,timeout,lemmas,posns)
    2.73 -  => (calls, success, time, timeout + 1, lemmas,posns))
    2.74 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.75 +  => (calls, success, proofs, time, timeout + 1, lemmas,posns))
    2.76  
    2.77  fun inc_metis_lemmas n = map_me_data
    2.78 - (fn (calls,success,time,timeout,lemmas,posns)
    2.79 -  => (calls, success, time, timeout, lemmas + n, posns))
    2.80 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.81 +  => (calls, success, proofs, time, timeout, lemmas + n, posns))
    2.82  
    2.83  fun inc_metis_posns pos = map_me_data
    2.84 - (fn (calls,success,time,timeout,lemmas,posns)
    2.85 -  => (calls, success, time, timeout, lemmas, pos::posns))
    2.86 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.87 +  => (calls, success, proofs, time, timeout, lemmas, pos::posns))
    2.88  
    2.89  val inc_metis_calls0 = map_me_data0 
    2.90 -(fn (calls, success, time, timeout, lemmas,posns)
    2.91 -  => (calls + 1, success, time, timeout, lemmas,posns))
    2.92 +(fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.93 +  => (calls + 1, success, proofs, time, timeout, lemmas,posns))
    2.94  
    2.95  val inc_metis_success0 = map_me_data0
    2.96 - (fn (calls,success,time,timeout,lemmas,posns)
    2.97 -  => (calls, success + 1, time, timeout, lemmas,posns))
    2.98 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    2.99 +  => (calls, success + 1, proofs, time, timeout, lemmas,posns))
   2.100 +
   2.101 +val inc_metis_proofs0 = map_me_data0
   2.102 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   2.103 +  => (calls, success, proofs + 1, time, timeout, lemmas,posns))
   2.104  
   2.105  fun inc_metis_time0 t = map_me_data0
   2.106 - (fn (calls,success,time,timeout,lemmas,posns)
   2.107 -  => (calls, success, time + t, timeout, lemmas,posns))
   2.108 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   2.109 +  => (calls, success, proofs, time + t, timeout, lemmas,posns))
   2.110  
   2.111  val inc_metis_timeout0 = map_me_data0
   2.112 - (fn (calls,success,time,timeout,lemmas,posns)
   2.113 -  => (calls, success, time, timeout + 1, lemmas,posns))
   2.114 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   2.115 +  => (calls, success, proofs, time, timeout + 1, lemmas,posns))
   2.116  
   2.117  fun inc_metis_lemmas0 n = map_me_data0
   2.118 - (fn (calls,success,time,timeout,lemmas,posns)
   2.119 -  => (calls, success, time, timeout, lemmas + n, posns))
   2.120 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   2.121 +  => (calls, success, proofs, time, timeout, lemmas + n, posns))
   2.122  
   2.123  fun inc_metis_posns0 pos = map_me_data0
   2.124 - (fn (calls,success,time,timeout,lemmas,posns)
   2.125 -  => (calls, success, time, timeout, lemmas, pos::posns))
   2.126 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   2.127 +  => (calls, success, proofs, time, timeout, lemmas, pos::posns))
   2.128  
   2.129  local
   2.130  
   2.131 @@ -190,10 +199,10 @@
   2.132    let val str0 = string_of_int o the_default 0
   2.133    in str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) end
   2.134  
   2.135 -fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_time
   2.136 +fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_proofs metis_time
   2.137      metis_timeout metis_lemmas metis_posns =
   2.138   (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
   2.139 -  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success);
   2.140 +  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^ " (proof: " ^ str metis_proofs ^ ")");
   2.141    log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
   2.142    log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
   2.143    log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
   2.144 @@ -216,11 +225,11 @@
   2.145  fun log_data id log (Data
   2.146     (ShData{calls=sh_calls, lemmas=sh_lemmas, success=sh_success,
   2.147        time_isa=sh_time_isa,time_atp=sh_time_atp,time_atp_fail=sh_time_atp_fail},
   2.148 -    MeData{calls=metis_calls0,
   2.149 +    MeData{calls=metis_calls0, proofs=metis_proofs0,
   2.150        success=metis_success0, time=metis_time0, timeout=metis_timeout0,
   2.151        lemmas=metis_lemmas0,posns=metis_posns0},
   2.152      MinData{succs=min_succs, ab_ratios=ab_ratios, it_ratios=it_ratios},
   2.153 -    MeData{calls=metis_calls,
   2.154 +    MeData{calls=metis_calls, proofs=metis_proofs,
   2.155        success=metis_success, time=metis_time, timeout=metis_timeout,
   2.156        lemmas=metis_lemmas,posns=metis_posns})) =
   2.157    if sh_calls > 0
   2.158 @@ -229,12 +238,12 @@
   2.159      log_sh_data log sh_calls sh_success sh_lemmas sh_time_isa sh_time_atp sh_time_atp_fail;
   2.160      log "";
   2.161      if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls
   2.162 -      metis_success metis_time metis_timeout metis_lemmas  metis_posns else ();
   2.163 +      metis_success metis_proofs metis_time metis_timeout metis_lemmas  metis_posns else ();
   2.164      log "";
   2.165      if metis_calls0 > 0
   2.166        then (log_min_data log min_succs ab_ratios it_ratios; log "";
   2.167              log_metis_data log "unminimized " sh_calls sh_success metis_calls0
   2.168 -              metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
   2.169 +              metis_success0 metis_proofs0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
   2.170        else ()
   2.171     )
   2.172    else ()
   2.173 @@ -376,8 +385,8 @@
   2.174    end
   2.175  
   2.176  
   2.177 -fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout,
   2.178 -    inc_metis_lemmas, inc_metis_posns) args named_thms id
   2.179 +fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time, inc_metis_timeout,
   2.180 +    inc_metis_lemmas, inc_metis_posns) args name named_thms id
   2.181      ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   2.182    let
   2.183      fun metis thms ctxt = MetisTools.metis_tac ctxt thms
   2.184 @@ -388,6 +397,7 @@
   2.185            change_data id (inc_metis_lemmas (length named_thms));
   2.186            change_data id (inc_metis_time t);
   2.187            change_data id (inc_metis_posns pos);
   2.188 +          if name = "proof" then change_data id inc_metis_proofs else ();
   2.189            "succeeded (" ^ string_of_int t ^ ")")
   2.190      fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
   2.191        handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
   2.192 @@ -401,13 +411,13 @@
   2.193      |> log o prefix (metis_tag id) 
   2.194    end
   2.195  
   2.196 -fun sledgehammer_action args id (st as {log, pre, ...}: Mirabelle.run_args) =
   2.197 +fun sledgehammer_action args id (st as {log, pre, name, ...}: Mirabelle.run_args) =
   2.198    if can Logic.dest_conjunction (Thm.major_prem_of(snd(snd(Proof.get_goal pre))))
   2.199    then () else
   2.200    let
   2.201 -    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
   2.202 +    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time,
   2.203          inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
   2.204 -    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0,
   2.205 +    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_proofs0, inc_metis_time0,
   2.206          inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
   2.207      val named_thms = ref (NONE : (string * thm list) list option)
   2.208      val minimize = AList.defined (op =) args minimizeK
   2.209 @@ -416,12 +426,12 @@
   2.210      if is_some (!named_thms)
   2.211        then
   2.212         (if minimize
   2.213 -          then Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))) id st
   2.214 +          then Mirabelle.catch metis_tag (run_metis metis0_fns args name (these (!named_thms))) id st
   2.215            else ();
   2.216         if minimize andalso not(null(these(!named_thms)))
   2.217           then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st
   2.218           else ();
   2.219 -       Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st)
   2.220 +       Mirabelle.catch metis_tag (run_metis metis_fns args name (these (!named_thms))) id st)
   2.221      else ()
   2.222    end
   2.223