src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
author nipkow
Mon, 14 Sep 2009 19:30:48 +0200
changeset 32571 d4bb776874b8
parent 32567 de411627a985
child 32574 719426c9e1eb
permissions -rw-r--r--
count number of iterations required for minimization (and fixed bug: minimization was always called)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32564
378528d2f7eb standard headers and text sections;
wenzelm
parents: 32551
diff changeset
     1
(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
378528d2f7eb standard headers and text sections;
wenzelm
parents: 32551
diff changeset
     2
    Author:     Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich
32385
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"
32541
cea1716eb106 timeout option for ATPs
boehmes
parents: 32536
diff changeset
     9
val prover_timeoutK = "prover_timeout"
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    10
val keepK = "keep"
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
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    22
datatype sh_data = ShData of {
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    23
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    24
  success: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    25
  time_isa: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    26
  time_atp: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    27
  time_atp_fail: int}
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    28
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    29
datatype me_data = MeData of {
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    30
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    31
  success: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    32
  time: int,
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    33
  timeout: int,
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
    34
  lemmas: int,
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
    35
  posns: Position.T list
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    36
  }
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    37
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    38
datatype min_data = MinData of {
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    39
  calls: int,
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    40
  ratios: int
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    41
  }
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    42
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    43
(* The first me_data component is only used if "minimize" is on.
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    44
   Then it records how metis behaves with un-minimized lemmas.
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    45
*)
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    46
datatype data = Data of sh_data * me_data * min_data * me_data
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    47
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    48
fun make_sh_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) =
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    49
  ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    50
    time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    51
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    52
fun make_min_data (calls, ratios) =
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    53
  MinData{calls=calls, ratios=ratios}
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    54
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
    55
fun make_me_data (calls, success, time, timeout, lemmas, posns) =
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
    56
  MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    57
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    58
val empty_data =
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    59
  Data(make_sh_data (0, 0, 0, 0, 0),
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    60
       make_me_data(0, 0, 0, 0, 0, []),
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    61
       MinData{calls=0, ratios=0},
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    62
       make_me_data(0, 0, 0, 0, 0, []))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    63
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    64
fun map_sh_data f
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    65
  (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) =
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    66
  Data (make_sh_data (f (calls, success, time_isa, time_atp, time_atp_fail)),
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    67
        meda0, minda, meda)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    68
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    69
fun map_min_data f
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    70
  (Data(shda, meda0, MinData{calls,ratios}, meda)) =
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    71
  Data(shda, meda0, make_min_data(f(calls,ratios)), meda)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    72
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    73
fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) =
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    74
  Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda)
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    75
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    76
fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,time,timeout,lemmas,posns})) =
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    77
  Data(shda, meda0, minda, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    78
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
    79
val inc_sh_calls =
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    80
  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    81
    => (calls + 1, success, time_isa, time_atp, time_atp_fail))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    82
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
    83
val inc_sh_success =
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    84
  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    85
    => (calls, success + 1, time_isa, time_atp, time_atp_fail))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    86
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
    87
fun inc_sh_time_isa t =
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    88
  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    89
    => (calls, success, time_isa + t, time_atp, time_atp_fail))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    90
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
    91
fun inc_sh_time_atp t =
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    92
  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    93
    => (calls, success, time_isa, time_atp + t, time_atp_fail))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    94
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
    95
fun inc_sh_time_atp_fail t =
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    96
  map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    97
    => (calls, success, time_isa, time_atp, time_atp_fail + t))
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    98
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    99
val inc_min_calls =
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   100
  map_min_data (fn (calls, ratios) => (calls + 1, ratios))
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   101
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   102
fun inc_min_ratios n =
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   103
  map_min_data (fn (calls, ratios) => (calls, ratios + n))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   104
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   105
val inc_metis_calls = map_me_data
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   106
 (fn (calls, success, time, timeout, lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   107
  => (calls + 1, success, time, timeout, lemmas,posns))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   108
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   109
val inc_metis_success = map_me_data
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   110
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   111
  => (calls, success + 1, time, timeout, lemmas,posns))
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   112
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   113
fun inc_metis_time t = map_me_data
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   114
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   115
  => (calls, success, time + t, timeout, lemmas,posns))
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   116
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   117
val inc_metis_timeout = map_me_data
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   118
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   119
  => (calls, success, time, timeout + 1, lemmas,posns))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   120
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   121
fun inc_metis_lemmas n = map_me_data
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   122
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   123
  => (calls, success, time, timeout, lemmas + n, posns))
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
   124
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   125
fun inc_metis_posns pos = map_me_data
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   126
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   127
  => (calls, success, time, timeout, lemmas, pos::posns))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   128
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   129
val inc_metis_calls0 = map_me_data0 
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   130
(fn (calls, success, time, timeout, lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   131
  => (calls + 1, success, time, timeout, lemmas,posns))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   132
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   133
val inc_metis_success0 = map_me_data0
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   134
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   135
  => (calls, success + 1, time, timeout, lemmas,posns))
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   136
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   137
fun inc_metis_time0 t = map_me_data0
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   138
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   139
  => (calls, success, time + t, timeout, lemmas,posns))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   140
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   141
val inc_metis_timeout0 = map_me_data0
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   142
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   143
  => (calls, success, time, timeout + 1, lemmas,posns))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   144
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   145
fun inc_metis_lemmas0 n = map_me_data0
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   146
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   147
  => (calls, success, time, timeout, lemmas + n, posns))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   148
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   149
fun inc_metis_posns0 pos = map_me_data0
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   150
 (fn (calls,success,time,timeout,lemmas,posns)
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   151
  => (calls, success, time, timeout, lemmas, pos::posns))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   152
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   153
local
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
val str = string_of_int
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   156
val str3 = Real.fmt (StringCvt.FIX (SOME 3))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   157
fun percentage a b = string_of_int (a * 100 div b)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   158
fun time t = Real.fromInt t / 1000.0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   159
fun avg_time t n =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   160
  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
   161
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   162
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
   163
 (log ("Total number of sledgehammer calls: " ^ str sh_calls);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   164
  log ("Number of successful sledgehammer calls: " ^ str sh_success);
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   165
  log ("Success rate: " ^ percentage sh_success sh_calls ^ "%");
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   166
  log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time sh_time_isa));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   167
  log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time sh_time_atp));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   168
  log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time sh_time_atp_fail));
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   169
  log ("Average time for sledgehammer calls (Isabelle): " ^
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   170
    str3 (avg_time sh_time_isa sh_calls));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   171
  log ("Average time for successful sledgehammer calls (ATP): " ^
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   172
    str3 (avg_time sh_time_atp sh_success));
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   173
  log ("Average time for failed sledgehammer calls (ATP): " ^
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   174
    str3 (avg_time sh_time_atp_fail (sh_calls - sh_success)))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   175
  )
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   176
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   177
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   178
fun str_of_pos pos =
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   179
  let val str0 = string_of_int o the_default 0
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   180
  in str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) end
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   181
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   182
fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_time
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   183
    metis_timeout metis_lemmas metis_posns =
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   184
 (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   185
  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success);
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   186
  log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   187
  log ("Number of " ^ tag ^ "metis exceptions: " ^
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   188
    str (sh_success - metis_success - metis_timeout));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   189
  log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
   190
  log ("Number of " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   191
  log ("Total time for successful metis calls: " ^ str3 (time metis_time));
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   192
  log ("Average time for successful metis calls: " ^
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   193
    str3 (avg_time metis_time metis_success));
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   194
  if tag=""
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   195
  then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns))
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   196
  else ()
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   197
 )
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   198
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   199
fun log_min_data log calls ratios =
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   200
  (log ("Number of minimizations: " ^ string_of_int calls);
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   201
   log ("Minimization ratios: " ^ string_of_int ratios)
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   202
  )
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   203
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   204
in
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   205
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   206
fun log_data id log (Data
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   207
   (ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa,
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   208
      time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail},
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   209
    MeData{calls=metis_calls0,
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   210
      success=metis_success0, time=metis_time0, timeout=metis_timeout0,
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   211
      lemmas=metis_lemmas0,posns=metis_posns0},
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   212
    MinData{calls=min_calls, ratios=min_ratios},
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   213
    MeData{calls=metis_calls,
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   214
      success=metis_success, time=metis_time, timeout=metis_timeout,
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   215
      lemmas=metis_lemmas,posns=metis_posns})) =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   216
  if sh_calls > 0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   217
  then
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   218
   (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   219
    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
   220
    log "";
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   221
    if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   222
      metis_success metis_time metis_timeout metis_lemmas  metis_posns else ();
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   223
    log "";
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   224
    if metis_calls0 > 0
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   225
      then (log_min_data log min_calls min_ratios; log "";
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   226
            log_metis_data log "unminimized " sh_calls sh_success metis_calls0
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   227
              metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   228
      else ()
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   229
   )
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   230
  else ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   231
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   232
end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   233
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
(* Warning: we implicitly assume single-threaded execution here! *)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   236
val data = ref ([] : (int * data) list)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   237
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   238
fun init id thy = (change data (cons (id, empty_data)); thy)
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   239
fun done id ({log, ...}: Mirabelle.done_args) =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   240
  AList.lookup (op =) (!data) id
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   241
  |> Option.map (log_data id log)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   242
  |> K ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   243
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   244
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
   245
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   246
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   247
fun get_atp thy args =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   248
  AList.lookup (op =) args proverK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   249
  |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   250
  |> (fn name => (name, the (AtpManager.get_prover name thy)))
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   251
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   252
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   253
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   254
fun safe init done f x =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   255
  let
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   256
    val y = init x
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   257
    val z = Exn.capture f y
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   258
    val _ = done y
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   259
  in Exn.release z end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   260
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   261
fun init_sh NONE = !AtpWrapper.destdir
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   262
  | init_sh (SOME path) =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   263
      let
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   264
        (* Warning: we implicitly assume single-threaded execution here! *)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   265
        val old = !AtpWrapper.destdir
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   266
        val _ = AtpWrapper.destdir := path
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   267
      in old end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   268
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   269
fun done_sh path = AtpWrapper.destdir := path
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   270
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   271
datatype sh_result =
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   272
  SH_OK of int * int * string list |
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   273
  SH_FAIL of int * int |
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   274
  SH_ERROR
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   275
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   276
fun run_sh (prover_name, prover) timeout st _ =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   277
  let
32541
cea1716eb106 timeout option for ATPs
boehmes
parents: 32536
diff changeset
   278
    val atp = prover timeout NONE NONE prover_name 1
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   279
    val ((success, (message, thm_names), time_atp, _, _, _), time_isa) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   280
      Mirabelle.cpu_time atp (Proof.get_goal st)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   281
  in
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   282
    if success then (message, SH_OK (time_isa, time_atp, thm_names))
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   283
    else (message, SH_FAIL(time_isa, time_atp))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   284
  end
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   285
  handle ResHolClause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   286
       | ERROR msg => ("error: " ^ msg, SH_ERROR)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   287
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   288
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
   289
  let
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   290
    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
   291
    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
   292
  in
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   293
    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
   294
    |> 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
   295
    |> 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
   296
    |> 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
   297
    |> 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
   298
    |> 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
   299
  end
32452
d84edd022efe apply metis with found theorems in case sledgehammer was successful
boehmes
parents: 32434
diff changeset
   300
32498
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   301
in
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   302
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   303
fun run_sledgehammer args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   304
  let
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   305
    val _ = change_data id inc_sh_calls
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   306
    val atp as (prover_name, _) = get_atp (Proof.theory_of st) args
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   307
    val dir = AList.lookup (op =) args keepK
32541
cea1716eb106 timeout option for ATPs
boehmes
parents: 32536
diff changeset
   308
    val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   309
    val (msg, result) = safe init_sh done_sh (run_sh atp timeout st) dir
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   310
  in
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   311
    case result of
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   312
      SH_OK (time_isa, time_atp, names) =>
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   313
        let
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   314
          val _ = change_data id inc_sh_success
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   315
          val _ = change_data id (inc_sh_time_isa time_isa)
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   316
          val _ = change_data id (inc_sh_time_atp time_atp)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   317
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   318
          fun get_thms name = (name, thms_of_name (Proof.context_of st) name)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   319
          val _ = named_thms := SOME (map get_thms names)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   320
        in
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   321
          log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   322
            string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   323
        end
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   324
    | SH_FAIL (time_isa, time_atp) =>
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   325
        let
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   326
          val _ = change_data id (inc_sh_time_isa time_isa)
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   327
          val _ = change_data id (inc_sh_time_atp_fail time_atp)
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   328
        in log (sh_tag id ^ "failed: " ^ msg) end
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   329
    | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   330
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   331
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   332
end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   333
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   334
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   335
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   336
  let
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   337
    val n0 = length (these (!named_thms))
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   338
    val (prover_name, prover) = get_atp (Proof.theory_of st) args
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   339
    val minimize = AtpMinimal.minimalize prover prover_name
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   340
    val timeout =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   341
      AList.lookup (op =) args minimize_timeoutK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   342
      |> Option.map (fst o read_int o explode)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   343
      |> the_default 5
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   344
    val _ = log separator
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   345
  in
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   346
    case minimize timeout st (these (!named_thms)) of
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   347
      (SOME (named_thms',its), msg) =>
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   348
        (change_data id inc_min_calls;
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   349
         change_data id (inc_min_ratios ((100*its) div n0));
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   350
         if length named_thms' = n0
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   351
         then log (minimize_tag id ^ "already minimal")
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   352
         else (named_thms := SOME named_thms';
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   353
               log (minimize_tag id ^ "succeeded:\n" ^ msg))
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   354
        )
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   355
    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   356
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   357
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   358
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   359
fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout,
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   360
    inc_metis_lemmas, inc_metis_posns) args named_thms id
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   361
    ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   362
  let
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   363
    fun metis thms ctxt = MetisTools.metis_tac ctxt thms
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   364
    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   365
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   366
    fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   367
      | with_time (true, t) = (change_data id inc_metis_success;
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   368
          change_data id (inc_metis_time t);
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   369
          change_data id (inc_metis_posns pos);
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   370
          "succeeded (" ^ string_of_int t ^ ")")
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   371
    fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   372
      handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   373
           | ERROR msg => "error: " ^ msg
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   374
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   375
    val _ = log separator
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   376
    val _ = change_data id inc_metis_calls
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
   377
    val _ = change_data id (inc_metis_lemmas (length named_thms))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   378
  in
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   379
    maps snd named_thms
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   380
    |> timed_metis
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   381
    |> log o prefix (metis_tag id) 
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   382
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   383
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   384
fun sledgehammer_action args id (st as {log, ...}: Mirabelle.run_args) =
32515
e7c0d3c0494a Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents: 32511
diff changeset
   385
  let
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   386
    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   387
        inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   388
    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0,
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   389
        inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   390
    val named_thms = ref (NONE : (string * thm list) list option)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   391
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   392
    fun if_enabled k f =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   393
      if AList.defined (op =) args k andalso is_some (!named_thms)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   394
      then f id st else ()
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   395
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   396
    val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   397
    val _ = if_enabled minimizeK
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   398
      (Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))))
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   399
    val _ = if_enabled minimizeK
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   400
      (Mirabelle.catch minimize_tag (run_minimize args named_thms))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   401
    val _ = if is_some (!named_thms)
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   402
      then Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   403
      else ()
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   404
  in () end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   405
32511
43d2ac4aa2de added option full_typed for sledgehammer action
boehmes
parents: 32510
diff changeset
   406
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
   407
  let
e7c0d3c0494a Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents: 32511
diff changeset
   408
    val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   409
  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
   410
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   411
end