src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
author nipkow
Mon, 07 Sep 2009 19:41:07 +0200
changeset 32536 ac56c62758d3
parent 32533 9735013cec72
child 32541 cea1716eb106
permissions -rw-r--r--
tuned stats
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     1
(* Title:  mirabelle_sledgehammer.ML
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     2
   Author: Jasmin Blanchette and Sascha Boehme
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     3
*)
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     4
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     5
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     6
struct
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     7
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
     8
val proverK = "prover"
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
     9
val keepK = "keep"
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    10
val metisK = "metis"
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    11
val full_typesK = "full_types"
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    12
val minimizeK = "minimize"
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    13
val minimize_timeoutK = "minimize_timeout"
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    14
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    15
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    16
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    17
fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): "
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    18
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    19
val separator = "-----"
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    20
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    21
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    22
datatype data = Data of {
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    23
  sh_calls: int,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    24
  sh_success: int,
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
    25
  sh_time_isa: int,
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
    26
  sh_time_atp: int,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    27
  sh_time_atp_fail: int,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    28
  metis_calls: int,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    29
  metis_success: int,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    30
  metis_time: int,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    31
  metis_timeout: int }
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    32
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    33
fun make_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    34
    metis_time, metis_timeout) =
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
    35
  Data {sh_calls=sh_calls, sh_success=sh_success, sh_time_isa=sh_time_isa,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    36
    sh_time_atp=sh_time_atp, sh_time_atp_fail=sh_time_atp_fail,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    37
    metis_calls=metis_calls, metis_success=metis_success,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    38
    metis_time=metis_time, metis_timeout=metis_timeout}
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    39
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    40
fun map_data f (Data {sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    41
    metis_success, metis_time, metis_timeout}) =
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    42
  make_data (f (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    43
    metis_time, metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    44
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    45
val empty_data = make_data (0, 0, 0, 0, 0, 0, 0, 0, 0)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    46
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    47
val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    48
  metis_success, metis_time, metis_timeout) => (sh_calls + 1, sh_success,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    49
  sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    50
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    51
val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    52
  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success + 1,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    53
  sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    54
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    55
fun inc_sh_time_isa t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    56
  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    57
  sh_time_isa + t, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    58
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    59
fun inc_sh_time_atp t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    60
  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    61
  sh_time_isa, sh_time_atp + t, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    62
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    63
fun inc_sh_time_atp_fail t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
    64
  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    65
  sh_time_isa, sh_time_atp, sh_time_atp_fail + t, metis_calls, metis_success, metis_time, metis_timeout))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
    66
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    67
val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    68
  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    69
  sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls + 1, metis_success, metis_time, metis_timeout))
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    70
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    71
val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    72
  metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    73
  sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success + 1, metis_time,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    74
  metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    75
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    76
fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    77
  metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    78
  sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time + t,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    79
  metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    80
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    81
val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    82
  metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    83
  sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    84
  metis_timeout + 1))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    85
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    86
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    87
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    88
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    89
val str = string_of_int
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    90
val str3 = Real.fmt (StringCvt.FIX (SOME 3))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    91
fun percentage a b = string_of_int (a * 100 div b)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    92
fun time t = Real.fromInt t / 1000.0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    93
fun avg_time t n =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    94
  if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    95
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
    96
fun log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    97
 (log ("Total number of sledgehammer calls: " ^ str sh_calls);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    98
  log ("Number of successful sledgehammer calls: " ^ str sh_success);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    99
  log ("Success rate: " ^ percentage sh_success sh_calls ^ "%");
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   100
  log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time sh_time_isa));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   101
  log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time sh_time_atp));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   102
  log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time sh_time_atp_fail));
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   103
  log ("Average time for sledgehammer calls (Isabelle): " ^
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   104
    str3 (avg_time sh_time_isa sh_calls));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   105
  log ("Average time for successful sledgehammer calls (ATP): " ^
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   106
    str3 (avg_time sh_time_atp sh_success));
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   107
  log ("Average time for failed sledgehammer calls (ATP): " ^
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   108
    str3 (avg_time sh_time_atp_fail (sh_calls - sh_success)))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   109
  )
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   110
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   111
fun log_metis_data log sh_calls sh_success metis_calls metis_success metis_time
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   112
    metis_timeout =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   113
 (log ("Total number of metis calls: " ^ str metis_calls);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   114
  log ("Number of successful metis calls: " ^ str metis_success);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   115
  log ("Number of metis timeouts: " ^ str metis_timeout);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   116
  log ("Number of metis exceptions: " ^
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   117
    str (sh_success - metis_success - metis_timeout));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   118
  log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   119
  log ("Total time for successful metis calls: " ^ str3 (time metis_time));
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   120
  log ("Average time for successful metis calls: " ^
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   121
    str3 (avg_time metis_time metis_success)))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   122
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   123
in
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   124
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   125
fun log_data id log (Data {sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   126
    metis_success, metis_time, metis_timeout}) =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   127
  if sh_calls > 0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   128
  then
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   129
   (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   130
    log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail;
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   131
    log "";
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   132
    if metis_calls > 0 then log_metis_data log sh_calls sh_success metis_calls
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   133
      metis_success metis_time metis_timeout else ())
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   134
  else ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   135
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   136
end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   137
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   138
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   139
(* Warning: we implicitly assume single-threaded execution here! *)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   140
val data = ref ([] : (int * data) list)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   141
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   142
fun init id thy = (change data (cons (id, empty_data)); thy)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   143
fun done id {log, ...} =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   144
  AList.lookup (op =) (!data) id
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   145
  |> Option.map (log_data id log)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   146
  |> K ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   147
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   148
fun change_data id f = (change data (AList.map_entry (op =) id f); ())
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   149
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   150
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   151
fun get_atp thy args =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   152
  AList.lookup (op =) args proverK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   153
  |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   154
  |> (fn name => (name, the (AtpManager.get_prover name thy)))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   155
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   156
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   157
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   158
fun safe init done f x =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   159
  let
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   160
    val y = init x
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   161
    val z = Exn.capture f y
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   162
    val _ = done y
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   163
  in Exn.release z end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   164
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   165
fun init_sh NONE = !AtpWrapper.destdir
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   166
  | init_sh (SOME path) =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   167
      let
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   168
        (* Warning: we implicitly assume single-threaded execution here! *)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   169
        val old = !AtpWrapper.destdir
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   170
        val _ = AtpWrapper.destdir := path
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   171
      in old end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   172
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   173
fun done_sh path = AtpWrapper.destdir := path
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   174
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   175
datatype sh_result =
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   176
  SH_OK of int * int * string list |
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   177
  SH_FAIL of int * int |
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   178
  SH_ERROR
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   179
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   180
fun run_sh (prover_name, prover) timeout st _ =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   181
  let
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   182
    val atp = prover (Time.toSeconds timeout) NONE NONE prover_name 1
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   183
    val ((success, (message, thm_names), time_atp, _, _, _), time_isa) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   184
      Mirabelle.cpu_time atp (Proof.get_goal st)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   185
  in
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   186
    if success then (message, SH_OK (time_isa, time_atp, thm_names))
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   187
    else (message, SH_FAIL(time_isa, time_atp))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   188
  end
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   189
  handle ResHolClause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   190
       | ERROR msg => ("error: " ^ msg, SH_ERROR)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   191
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   192
fun thms_of_name ctxt name =
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   193
  let
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   194
    val lex = OuterKeyword.get_lexicons
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   195
    val get = maps (ProofContext.get_fact ctxt o fst)
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   196
  in
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   197
    Source.of_string name
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   198
    |> Symbol.source {do_recover=false}
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   199
    |> OuterLex.source {do_recover=SOME false} lex Position.start
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   200
    |> OuterLex.source_proper
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   201
    |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   202
    |> Source.exhaust
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   203
  end
32452
d84edd022efe apply metis with found theorems in case sledgehammer was successful
boehmes
parents: 32434
diff changeset
   204
32498
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   205
in
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   206
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   207
fun run_sledgehammer args named_thms id {pre=st, timeout, log, ...} =
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   208
  let
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   209
    val _ = change_data id inc_sh_calls
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   210
    val atp as (prover_name, _) = get_atp (Proof.theory_of st) args
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   211
    val dir = AList.lookup (op =) args keepK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   212
    val (msg, result) = safe init_sh done_sh (run_sh atp timeout st) dir
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   213
  in
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   214
    case result of
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   215
      SH_OK (time_isa, time_atp, names) =>
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   216
        let
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   217
          val _ = change_data id inc_sh_success
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   218
          val _ = change_data id (inc_sh_time_isa time_isa)
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   219
          val _ = change_data id (inc_sh_time_atp time_atp)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   220
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   221
          fun get_thms name = (name, thms_of_name (Proof.context_of st) name)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   222
          val _ = named_thms := SOME (map get_thms names)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   223
        in
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   224
          log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   225
            string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   226
        end
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   227
    | SH_FAIL (time_isa, time_atp) =>
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   228
        let
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   229
          val _ = change_data id (inc_sh_time_isa time_isa)
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   230
          val _ = change_data id (inc_sh_time_atp_fail time_atp)
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   231
        in log (sh_tag id ^ "failed: " ^ msg) end
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   232
    | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   233
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   234
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   235
end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   236
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   237
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   238
fun run_minimize args named_thms id {pre=st, log, ...} =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   239
  let
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   240
    val (prover_name, prover) = get_atp (Proof.theory_of st) args
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   241
    val minimize = AtpMinimal.minimalize prover prover_name
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   242
    val timeout =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   243
      AList.lookup (op =) args minimize_timeoutK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   244
      |> Option.map (fst o read_int o explode)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   245
      |> the_default 5
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   246
    val _ = log separator
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   247
  in
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   248
    (case minimize timeout st (these (!named_thms)) of
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   249
      (SOME named_thms', msg) =>
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   250
        if length named_thms' = length (these (!named_thms))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   251
        then log (minimize_tag id ^ "already minimal")
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   252
        else
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   253
         (named_thms := SOME named_thms';
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   254
          log (minimize_tag id ^ "succeeded:\n" ^ msg))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   255
    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   256
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   257
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   258
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   259
fun run_metis args named_thms id {pre=st, timeout, log, ...} =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   260
  let
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   261
    fun metis thms ctxt = MetisTools.metis_tac ctxt thms
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   262
    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   263
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   264
    fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   265
      | with_time (true, t) = (change_data id inc_metis_success;
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   266
          change_data id (inc_metis_time t);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   267
          "succeeded (" ^ string_of_int t ^ ")")
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   268
    fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   269
      handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   270
           | ERROR msg => "error: " ^ msg
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   271
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   272
    val _ = log separator
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   273
    val _ = change_data id inc_metis_calls
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   274
  in
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   275
    maps snd named_thms
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   276
    |> timed_metis
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   277
    |> log o prefix (metis_tag id) 
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   278
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   279
32452
d84edd022efe apply metis with found theorems in case sledgehammer was successful
boehmes
parents: 32434
diff changeset
   280
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   281
fun sledgehammer_action args id (st as {log, ...}) =
32515
e7c0d3c0494a Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents: 32511
diff changeset
   282
  let
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   283
    val named_thms = ref (NONE : (string * thm list) list option)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   284
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   285
    fun if_enabled k f =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   286
      if AList.defined (op =) args k andalso is_some (!named_thms)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   287
      then f id st else ()
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   288
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   289
    val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   290
    val _ = if_enabled minimizeK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   291
      (Mirabelle.catch minimize_tag (run_minimize args named_thms))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   292
    val _ = if_enabled metisK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   293
      (Mirabelle.catch metis_tag (run_metis args (these (!named_thms))))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   294
  in () end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   295
32511
43d2ac4aa2de added option full_typed for sledgehammer action
boehmes
parents: 32510
diff changeset
   296
fun invoke args =
32515
e7c0d3c0494a Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents: 32511
diff changeset
   297
  let
32526
e6996fb0a774 enabled metis permanently, tuned stats
nipkow
parents: 32525
diff changeset
   298
    val args = (metisK,"yes") :: args; (* always enable metis *)
32515
e7c0d3c0494a Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents: 32511
diff changeset
   299
    val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   300
  in Mirabelle.register (init, sledgehammer_action args, done) end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   301
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   302
end