src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
author boehmes
Sat, 05 Sep 2009 22:01:31 +0200
changeset 32525 ea322e847633
parent 32523 ba397aa0ff5d
child 32526 e6996fb0a774
permissions -rw-r--r--
added signature ATP_MINIMAL, fixed AtpMinimal.minimalize for the trivial case, Mirabelle: added an option to minimize a theorem set found by sledgehammer, use timeout of sledgehammer instead of additional timeLimit
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,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    25
  sh_time: int,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    26
  metis_calls: int,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    27
  metis_success: int,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    28
  metis_time: int,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    29
  metis_timeout: int }
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    30
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    31
fun make_data (sh_calls, sh_success, sh_time, metis_calls, metis_success,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    32
    metis_time, metis_timeout) =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    33
  Data {sh_calls=sh_calls, sh_success=sh_success, sh_time=sh_time,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    34
    metis_calls=metis_calls, metis_success=metis_success,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    35
    metis_time=metis_time, metis_timeout=metis_timeout}
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    36
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    37
fun map_data f (Data {sh_calls, sh_success, sh_time, metis_calls,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    38
    metis_success, metis_time, metis_timeout}) =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    39
  make_data (f (sh_calls, sh_success, sh_time, metis_calls, metis_success,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    40
    metis_time, metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    41
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    42
val empty_data = make_data (0, 0, 0, 0, 0, 0, 0)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    43
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    44
val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    45
  metis_success, metis_time, metis_timeout) => (sh_calls + 1, sh_success,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    46
  sh_time, metis_calls, metis_success, metis_time, metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    47
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    48
val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    49
  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success + 1,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    50
  sh_time, metis_calls, metis_success, metis_time, metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    51
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    52
fun inc_sh_time t = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    53
  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    54
  sh_time + t, metis_calls, metis_success, metis_time, metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    55
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    56
val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    57
  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    58
  sh_time, metis_calls + 1, metis_success, metis_time, metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    59
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    60
val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    61
  metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    62
  sh_success, sh_time, metis_calls, metis_success + 1, metis_time,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    63
  metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    64
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    65
fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    66
  metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    67
  sh_success, sh_time, metis_calls, metis_success, metis_time + t,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    68
  metis_timeout))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    69
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    70
val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    71
  metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    72
  sh_success, sh_time, metis_calls, metis_success, metis_time,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    73
  metis_timeout + 1))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    74
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    75
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    76
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    77
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    78
val str = string_of_int
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    79
val str3 = Real.fmt (StringCvt.FIX (SOME 3))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    80
fun percentage a b = string_of_int (a * 100 div b)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    81
fun time t = Real.fromInt t / 1000.0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    82
fun avg_time t n =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    83
  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
    84
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    85
fun log_sh_data log sh_calls sh_success sh_time =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    86
 (log ("Total number of sledgehammer calls: " ^ str sh_calls);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    87
  log ("Number of successful sledgehammer calls: " ^ str sh_success);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    88
  log ("Success rate: " ^ percentage sh_success sh_calls ^ "%");
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    89
  log ("Total time for successful sledgehammer calls: " ^ str3 (time sh_time));
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    90
  log ("Average time for successful sledgehammer calls: " ^
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    91
    str3 (avg_time sh_time sh_success)))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    92
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    93
fun log_metis_data log sh_success metis_calls metis_success metis_time
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    94
    metis_timeout =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    95
 (log ("Total number of metis calls: " ^ str metis_calls);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    96
  log ("Number of successful metis calls: " ^ str metis_success);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    97
  log ("Number of metis timeouts: " ^ str metis_timeout);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    98
  log ("Number of metis exceptions: " ^
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    99
    str (sh_success - metis_success - metis_timeout));
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   100
  log ("Success rate: " ^ percentage metis_success metis_calls ^ "%");
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   101
  log ("Total time for successful metis calls: " ^ str3 (time metis_time));
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   102
  log ("Average time for successful metis calls: " ^
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   103
    str3 (avg_time metis_time metis_success)))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   104
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   105
in
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   106
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   107
fun log_data id log (Data {sh_calls, sh_success, sh_time, metis_calls,
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   108
    metis_success, metis_time, metis_timeout}) =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   109
  if sh_calls > 0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   110
  then
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   111
   (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   112
    log_sh_data log sh_calls sh_success sh_time;
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   113
    log "";
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   114
    if metis_calls > 0 then log_metis_data log sh_success metis_calls
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   115
      metis_success metis_time metis_timeout else ())
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   116
  else ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   117
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   118
end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   119
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   120
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   121
(* Warning: we implicitly assume single-threaded execution here! *)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   122
val data = ref ([] : (int * data) list)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   123
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   124
fun init id thy = (change data (cons (id, empty_data)); thy)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   125
fun done id {log, ...} =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   126
  AList.lookup (op =) (!data) id
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   127
  |> Option.map (log_data id log)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   128
  |> K ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   129
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   130
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
   131
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   132
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   133
fun get_atp thy args =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   134
  AList.lookup (op =) args proverK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   135
  |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   136
  |> (fn name => (name, the (AtpManager.get_prover name thy)))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   137
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   138
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   139
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   140
fun safe init done f x =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   141
  let
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   142
    val y = init x
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   143
    val z = Exn.capture f y
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   144
    val _ = done y
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   145
  in Exn.release z end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   146
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   147
fun init_sh NONE = !AtpWrapper.destdir
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   148
  | init_sh (SOME path) =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   149
      let
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   150
        (* Warning: we implicitly assume single-threaded execution here! *)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   151
        val old = !AtpWrapper.destdir
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   152
        val _ = AtpWrapper.destdir := path
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   153
      in old end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   154
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   155
fun done_sh path = AtpWrapper.destdir := path
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   156
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   157
fun run_sh (prover_name, prover) timeout st _ =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   158
  let
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   159
    val atp = prover (Time.toSeconds timeout) NONE NONE prover_name 1
32523
ba397aa0ff5d separate output of ATP user time and sledgehammer (ML code) user time
boehmes
parents: 32521
diff changeset
   160
    val ((success, (message, thm_names), atp_time, _, _, _), sh_time) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   161
      Mirabelle.cpu_time atp (Proof.get_goal st)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   162
  in
32523
ba397aa0ff5d separate output of ATP user time and sledgehammer (ML code) user time
boehmes
parents: 32521
diff changeset
   163
    if success then (message, SOME (atp_time, sh_time, thm_names))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   164
    else (message, NONE)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   165
  end
32523
ba397aa0ff5d separate output of ATP user time and sledgehammer (ML code) user time
boehmes
parents: 32521
diff changeset
   166
  handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, 0, []))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   167
       | ERROR msg => ("error: " ^ msg, NONE)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   168
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   169
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
   170
  let
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   171
    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
   172
    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
   173
  in
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   174
    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
   175
    |> 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
   176
    |> 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
   177
    |> 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
   178
    |> 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
   179
    |> 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
   180
  end
32452
d84edd022efe apply metis with found theorems in case sledgehammer was successful
boehmes
parents: 32434
diff changeset
   181
32498
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   182
in
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   183
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   184
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
   185
  let
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   186
    val _ = change_data id inc_sh_calls 
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   187
    val atp as (prover_name, _) = get_atp (Proof.theory_of st) args
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   188
    val dir = AList.lookup (op =) args keepK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   189
    val (msg, result) = safe init_sh done_sh (run_sh atp timeout st) dir
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   190
  in
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   191
    (case result of
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   192
      SOME (atp_time, sh_time, names) =>
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   193
        let
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   194
          val _ = change_data id inc_sh_success
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   195
          val _ = change_data id (inc_sh_time (atp_time + sh_time))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   196
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   197
          fun get_thms name = (name, thms_of_name (Proof.context_of st) name)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   198
          val _ = named_thms := SOME (map get_thms names)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   199
        in
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   200
          log (sh_tag id ^ "succeeded (" ^ string_of_int atp_time ^ "+" ^
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   201
            string_of_int sh_time ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   202
        end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   203
    | NONE => log (sh_tag id ^ "failed: " ^ msg))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   204
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   205
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   206
end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   207
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   208
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   209
fun run_minimize args named_thms id {pre=st, log, ...} =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   210
  let
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   211
    val (prover_name, prover) = get_atp (Proof.theory_of st) args
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   212
    val minimize = AtpMinimal.minimalize prover prover_name
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   213
    val timeout =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   214
      AList.lookup (op =) args minimize_timeoutK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   215
      |> Option.map (fst o read_int o explode)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   216
      |> the_default 5
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   217
    val _ = log separator
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   218
  in
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   219
    (case minimize timeout st (these (!named_thms)) of
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   220
      (SOME named_thms', msg) =>
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   221
        if length named_thms' = length (these (!named_thms))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   222
        then log (minimize_tag id ^ "already minimal")
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   223
        else
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   224
         (named_thms := SOME named_thms';
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   225
          log (minimize_tag id ^ "succeeded:\n" ^ msg))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   226
    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   227
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   228
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   229
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   230
fun run_metis args named_thms id {pre=st, timeout, log, ...} =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   231
  let
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   232
    fun metis thms ctxt = MetisTools.metis_tac ctxt thms
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   233
    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   234
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   235
    fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   236
      | with_time (true, t) = (change_data id inc_metis_success;
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   237
          change_data id (inc_metis_time t);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   238
          "succeeded (" ^ string_of_int t ^ ")")
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   239
    fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   240
      handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   241
           | ERROR msg => "error: " ^ msg
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   242
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   243
    val _ = log separator
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   244
    val _ = change_data id inc_metis_calls
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   245
  in
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   246
    maps snd named_thms
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   247
    |> timed_metis
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   248
    |> log o prefix (metis_tag id) 
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   249
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   250
32452
d84edd022efe apply metis with found theorems in case sledgehammer was successful
boehmes
parents: 32434
diff changeset
   251
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   252
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
   253
  let
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   254
    val named_thms = ref (NONE : (string * thm list) list option)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   255
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   256
    fun if_enabled k f =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   257
      if AList.defined (op =) args k andalso is_some (!named_thms)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   258
      then f id st else ()
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   259
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   260
    val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   261
    val _ = if_enabled minimizeK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   262
      (Mirabelle.catch minimize_tag (run_minimize args named_thms))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   263
    val _ = if_enabled metisK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   264
      (Mirabelle.catch metis_tag (run_metis args (these (!named_thms))))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   265
  in () end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   266
32511
43d2ac4aa2de added option full_typed for sledgehammer action
boehmes
parents: 32510
diff changeset
   267
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
   268
  let
e7c0d3c0494a Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents: 32511
diff changeset
   269
    val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   270
  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
   271
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   272
end