src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
author blanchet
Mon, 26 Jul 2010 14:14:24 +0200
changeset 37994 b04307085a09
parent 37631 16048a884a2c
child 38015 b30c3c2e1030
permissions -rw-r--r--
make TPTP generator accept full first-order formulas
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"
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
    10
val prover_hard_timeoutK = "prover_hard_timeout"
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    11
val keepK = "keep"
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    12
val full_typesK = "full_types"
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    13
val minimizeK = "minimize"
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    14
val minimize_timeoutK = "minimize_timeout"
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    15
val metis_ftK = "metis_ft"
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    16
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    17
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    18
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    19
fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): "
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    20
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    21
val separator = "-----"
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    22
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    23
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    24
datatype sh_data = ShData of {
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    25
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    26
  success: int,
32585
e788b33dd2b4 revised lemma counting
nipkow
parents: 32574
diff changeset
    27
  lemmas: int,
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    28
  max_lems: int,
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    29
  time_isa: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    30
  time_atp: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    31
  time_atp_fail: int}
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    32
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    33
datatype me_data = MeData of {
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    34
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    35
  success: int,
32676
b1c85a117dec record how many "proof"s are solved by s/h
nipkow
parents: 32612
diff changeset
    36
  proofs: int,
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    37
  time: int,
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    38
  timeout: int,
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
    39
  lemmas: int * int * int,
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
    40
  posns: Position.T list
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    41
  }
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    42
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    43
datatype min_data = MinData of {
32609
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
    44
  succs: int,
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    45
  ab_ratios: int
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    46
  }
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    47
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    48
fun make_sh_data
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    49
      (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail) =
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    50
  ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    51
         time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    52
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    53
fun make_min_data (succs, ab_ratios) =
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    54
  MinData{succs=succs, ab_ratios=ab_ratios}
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    55
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
    56
fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) =
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    57
  MeData{calls=calls, success=success, proofs=proofs, time=time,
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
    58
         timeout=timeout, lemmas=lemmas, posns=posns}
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    59
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    60
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0)
35871
c93bda4fdf15 remove the iteration counter from Sledgehammer's minimizer
blanchet
parents: 35867
diff changeset
    61
val empty_min_data = make_min_data (0, 0)
c93bda4fdf15 remove the iteration counter from Sledgehammer's minimizer
blanchet
parents: 35867
diff changeset
    62
val empty_me_data = make_me_data (0, 0, 0, 0, 0, (0,0,0), [])
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    63
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    64
fun tuple_of_sh_data (ShData {calls, success, lemmas, max_lems, time_isa,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    65
  time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    66
  time_atp, time_atp_fail)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    67
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    68
fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    69
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    70
fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    71
  posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    72
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    73
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    74
datatype metis = Unminimized | Minimized | UnminimizedFT | MinimizedFT
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    75
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    76
datatype data = Data of {
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    77
  sh: sh_data,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    78
  min: min_data,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    79
  me_u: me_data, (* metis with unminimized set of lemmas *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    80
  me_m: me_data, (* metis with minimized set of lemmas *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    81
  me_uft: me_data, (* metis with unminimized set of lemmas and fully-typed *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    82
  me_mft: me_data, (* metis with minimized set of lemmas and fully-typed *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    83
  mini: bool   (* with minimization *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    84
  }
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    85
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    86
fun make_data (sh, min, me_u, me_m, me_uft, me_mft, mini) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    87
  Data {sh=sh, min=min, me_u=me_u, me_m=me_m, me_uft=me_uft, me_mft=me_mft,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    88
    mini=mini}
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    89
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    90
val empty_data = make_data (empty_sh_data, empty_min_data,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    91
  empty_me_data, empty_me_data, empty_me_data, empty_me_data, false)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    92
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    93
fun map_sh_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    94
  let val sh' = make_sh_data (f (tuple_of_sh_data sh))
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    95
  in make_data (sh', min, me_u, me_m, me_uft, me_mft, mini) end
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    96
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    97
fun map_min_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    98
  let val min' = make_min_data (f (tuple_of_min_data min))
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    99
  in make_data (sh, min', me_u, me_m, me_uft, me_mft, mini) end
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   100
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   101
fun map_me_data f m (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   102
  let
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   103
    fun map_me g Unminimized   (u, m, uft, mft) = (g u, m, uft, mft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   104
      | map_me g Minimized     (u, m, uft, mft) = (u, g m, uft, mft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   105
      | map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   106
      | map_me g MinimizedFT   (u, m, uft, mft) = (u, m, uft, g mft)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   107
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   108
    val f' = make_me_data o f o tuple_of_me_data
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   109
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   110
    val (me_u', me_m', me_uft', me_mft') =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   111
      map_me f' m (me_u, me_m, me_uft, me_mft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   112
  in make_data (sh, min, me_u', me_m', me_uft', me_mft', mini) end
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   113
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   114
fun set_mini mini (Data {sh, min, me_u, me_m, me_uft, me_mft, ...}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   115
  make_data (sh, min, me_u, me_m, me_uft, me_mft, mini)
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   116
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   117
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   118
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   119
val inc_sh_calls =  map_sh_data
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   120
  (fn (calls, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   121
    => (calls + 1, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   122
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   123
val inc_sh_success = map_sh_data
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   124
  (fn (calls, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   125
    => (calls, success + 1, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
32585
e788b33dd2b4 revised lemma counting
nipkow
parents: 32574
diff changeset
   126
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   127
fun inc_sh_lemmas n = map_sh_data
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   128
  (fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   129
    => (calls,success,lemmas+n,max_lems,time_isa,time_atp,time_atp_fail))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   130
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   131
fun inc_sh_max_lems n = map_sh_data
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   132
  (fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   133
    => (calls,success,lemmas,Int.max(max_lems,n),time_isa,time_atp,time_atp_fail))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   134
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   135
fun inc_sh_time_isa t = map_sh_data
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   136
  (fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   137
    => (calls,success,lemmas,max_lems,time_isa + t,time_atp,time_atp_fail))
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   138
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   139
fun inc_sh_time_atp t = map_sh_data
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   140
  (fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   141
    => (calls,success,lemmas,max_lems,time_isa,time_atp + t,time_atp_fail))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   142
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   143
fun inc_sh_time_atp_fail t = map_sh_data
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   144
  (fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   145
    => (calls,success,lemmas,max_lems,time_isa,time_atp,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
   146
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   147
val inc_min_succs = map_min_data
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   148
  (fn (succs,ab_ratios) => (succs+1, ab_ratios))
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   149
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   150
fun inc_min_ab_ratios r = map_min_data
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   151
  (fn (succs, ab_ratios) => (succs, ab_ratios+r))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   152
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   153
val inc_metis_calls = map_me_data
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   154
  (fn (calls,success,proofs,time,timeout,lemmas,posns)
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   155
    => (calls + 1, success, proofs, time, timeout, lemmas,posns))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   156
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   157
val inc_metis_success = map_me_data
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   158
  (fn (calls,success,proofs,time,timeout,lemmas,posns)
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   159
    => (calls, success + 1, proofs, time, timeout, lemmas,posns))
32676
b1c85a117dec record how many "proof"s are solved by s/h
nipkow
parents: 32612
diff changeset
   160
b1c85a117dec record how many "proof"s are solved by s/h
nipkow
parents: 32612
diff changeset
   161
val inc_metis_proofs = map_me_data
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   162
  (fn (calls,success,proofs,time,timeout,lemmas,posns)
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   163
    => (calls, success, proofs + 1, time, timeout, lemmas,posns))
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   164
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   165
fun inc_metis_time m t = map_me_data
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   166
 (fn (calls,success,proofs,time,timeout,lemmas,posns)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   167
  => (calls, success, proofs, time + t, timeout, lemmas,posns)) m
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   168
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   169
val inc_metis_timeout = map_me_data
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   170
  (fn (calls,success,proofs,time,timeout,lemmas,posns)
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   171
    => (calls, success, proofs, time, timeout + 1, lemmas,posns))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   172
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   173
fun inc_metis_lemmas m n = map_me_data
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   174
  (fn (calls,success,proofs,time,timeout,lemmas,posns)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   175
    => (calls, success, proofs, time, timeout, inc_max n lemmas, posns)) m
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   176
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   177
fun inc_metis_posns m pos = map_me_data
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   178
  (fn (calls,success,proofs,time,timeout,lemmas,posns)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   179
    => (calls, success, proofs, time, timeout, lemmas, pos::posns)) m
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   180
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   181
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   182
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   183
val str = string_of_int
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   184
val str3 = Real.fmt (StringCvt.FIX (SOME 3))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   185
fun percentage a b = string_of_int (a * 100 div b)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   186
fun time t = Real.fromInt t / 1000.0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   187
fun avg_time t n =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   188
  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
   189
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   190
fun log_sh_data log
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   191
    (calls, success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) =
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   192
 (log ("Total number of sledgehammer calls: " ^ str calls);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   193
  log ("Number of successful sledgehammer calls: " ^ str success);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   194
  log ("Number of sledgehammer lemmas: " ^ str lemmas);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   195
  log ("Max number of sledgehammer lemmas: " ^ str max_lems);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   196
  log ("Success rate: " ^ percentage success calls ^ "%");
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   197
  log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   198
  log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_atp));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   199
  log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_atp_fail));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   200
  log ("Average time for sledgehammer calls (Isabelle): " ^
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   201
    str3 (avg_time time_isa calls));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   202
  log ("Average time for successful sledgehammer calls (ATP): " ^
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   203
    str3 (avg_time time_atp success));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   204
  log ("Average time for failed sledgehammer calls (ATP): " ^
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   205
    str3 (avg_time time_atp_fail (calls - success)))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   206
  )
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   207
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   208
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   209
fun str_of_pos pos =
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   210
  let val str0 = string_of_int o the_default 0
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   211
  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
   212
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   213
fun log_me_data log tag sh_calls (metis_calls, metis_success,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   214
    metis_proofs, metis_time, metis_timeout, (lemmas, lems_sos, lems_max),
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   215
    metis_posns) =
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   216
 (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   217
  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   218
    " (proof: " ^ str metis_proofs ^ ")");
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   219
  log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   220
  log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   221
  log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str lemmas);
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   222
  log ("SOS of successful " ^ tag ^ "metis lemmas: " ^ str lems_sos);
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   223
  log ("Max number of successful " ^ tag ^ "metis lemmas: " ^ str lems_max);
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   224
  log ("Total time for successful " ^ tag ^ "metis calls: " ^ str3 (time metis_time));
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   225
  log ("Average time for successful " ^ tag ^ "metis calls: " ^
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   226
    str3 (avg_time metis_time metis_success));
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   227
  if tag=""
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   228
  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
   229
  else ()
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   230
 )
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   231
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   232
fun log_min_data log (succs, ab_ratios) =
32609
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
   233
  (log ("Number of successful minimizations: " ^ string_of_int succs);
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   234
   log ("After/before ratios: " ^ string_of_int ab_ratios)
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   235
  )
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   236
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   237
in
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   238
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   239
fun log_data id log (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   240
  let
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   241
    val ShData {calls=sh_calls, ...} = sh
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   242
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   243
    fun app_if (MeData {calls, ...}) f = if calls > 0 then f () else ()
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   244
    fun log_me tag m =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   245
      log_me_data log tag sh_calls (tuple_of_me_data m)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   246
    fun log_metis (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   247
      (log_me tag1 m1; log ""; app_if m2 (fn () => log_me tag2 m2)))
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   248
  in
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   249
    if sh_calls > 0
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   250
    then
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   251
     (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   252
      log_sh_data log (tuple_of_sh_data sh);
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   253
      log "";
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   254
      if not mini
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   255
      then log_metis ("", me_u) ("fully-typed ", me_uft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   256
      else
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   257
        app_if me_u (fn () =>
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   258
         (log_metis ("unminimized ", me_u) ("unminimized fully-typed ", me_uft);
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   259
          log "";
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   260
          app_if me_m (fn () =>
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   261
            (log_min_data log (tuple_of_min_data min); log "";
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   262
             log_metis ("", me_m) ("fully-typed ", me_mft))))))
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   263
    else ()
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   264
  end
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   265
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   266
end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   267
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
(* Warning: we implicitly assume single-threaded execution here! *)
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   270
val data = Unsynchronized.ref ([] : (int * data) list)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   271
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   272
fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy)
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   273
fun done id ({log, ...}: Mirabelle.done_args) =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   274
  AList.lookup (op =) (!data) id
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   275
  |> Option.map (log_data id log)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   276
  |> K ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   277
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   278
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   279
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   280
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   281
fun get_atp thy args =
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   282
  let
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   283
    fun default_atp_name () =
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   284
      hd (#atps (Sledgehammer_Isar.default_params thy []))
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   285
      handle Empty => error "No ATP available."
36405
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   286
    fun get_prover name = (name, ATP_Manager.get_prover thy name)
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   287
  in
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   288
    (case AList.lookup (op =) args proverK of
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   289
      SOME name => get_prover name
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   290
    | NONE => get_prover (default_atp_name ()))
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   291
  end
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   292
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   293
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   294
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   295
datatype sh_result =
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   296
  SH_OK of int * int * string list |
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   297
  SH_FAIL of int * int |
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   298
  SH_ERROR
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   299
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32819
diff changeset
   300
fun run_sh prover hard_timeout timeout dir st =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   301
  let
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   302
    val {context = ctxt, facts, goal} = Proof.goal st
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   303
    val thy = ProofContext.theory_of ctxt
36405
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   304
    val change_dir = (fn SOME d => Config.put ATP_Systems.dest_dir d | _ => I)
33247
ed1681284f62 measure runtime of ATPs only if requested
boehmes
parents: 33016
diff changeset
   305
    val ctxt' =
ed1681284f62 measure runtime of ATPs only if requested
boehmes
parents: 33016
diff changeset
   306
      ctxt
ed1681284f62 measure runtime of ATPs only if requested
boehmes
parents: 33016
diff changeset
   307
      |> change_dir dir
36405
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   308
      |> Config.put ATP_Systems.measure_runtime true
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   309
    val params = Sledgehammer_Isar.default_params thy []
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   310
    val problem =
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   311
      {subgoal = 1, goal = (ctxt', (facts, goal)),
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   312
       relevance_override = {add = [], del = [], only = false},
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   313
       axiom_clauses = NONE, filtered_clauses = NONE}
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   314
    val time_limit =
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   315
      (case hard_timeout of
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   316
        NONE => I
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   317
      | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
36405
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   318
    val ({outcome, message, relevant_thm_names,
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   319
          atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result,
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   320
        time_isa) = time_limit (Mirabelle.cpu_time
36294
59a55dfa76d5 compile
blanchet
parents: 36223
diff changeset
   321
                      (prover params (K "") (Time.fromSeconds timeout))) problem
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   322
  in
36405
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   323
    case outcome of
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   324
      NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   325
    | SOME _ => (message, SH_FAIL (time_isa, time_atp))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   326
  end
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37631
diff changeset
   327
  handle ERROR msg => ("error: " ^ msg, SH_ERROR)
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   328
       | TimeLimit.TimeOut => ("timeout", SH_ERROR)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   329
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   330
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
   331
  let
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36959
diff changeset
   332
    val lex = Keyword.get_lexicons
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   333
    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
   334
  in
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   335
    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
   336
    |> Symbol.source {do_recover=false}
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36954
diff changeset
   337
    |> Token.source {do_recover=SOME false} lex Position.start
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36954
diff changeset
   338
    |> Token.source_proper
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36954
diff changeset
   339
    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   340
    |> 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
   341
  end
32452
d84edd022efe apply metis with found theorems in case sledgehammer was successful
boehmes
parents: 32434
diff changeset
   342
32498
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   343
in
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   344
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   345
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
   346
  let
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   347
    val _ = change_data id inc_sh_calls
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32819
diff changeset
   348
    val (prover_name, prover) = get_atp (Proof.theory_of st) args
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   349
    val dir = AList.lookup (op =) args keepK
32541
cea1716eb106 timeout option for ATPs
boehmes
parents: 32536
diff changeset
   350
    val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   351
    val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   352
      |> Option.map (fst o read_int o explode)
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32819
diff changeset
   353
    val (msg, result) = run_sh prover hard_timeout timeout dir st
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   354
  in
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   355
    case result of
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   356
      SH_OK (time_isa, time_atp, names) =>
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   357
        let fun get_thms name = (name, thms_of_name (Proof.context_of st) name)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   358
        in
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   359
          change_data id inc_sh_success;
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   360
          change_data id (inc_sh_lemmas (length names));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   361
          change_data id (inc_sh_max_lems (length names));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   362
          change_data id (inc_sh_time_isa time_isa);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   363
          change_data id (inc_sh_time_atp time_atp);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   364
          named_thms := SOME (map get_thms names);
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   365
          log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   366
            string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   367
        end
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   368
    | SH_FAIL (time_isa, time_atp) =>
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   369
        let
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   370
          val _ = change_data id (inc_sh_time_isa time_isa)
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   371
          val _ = change_data id (inc_sh_time_atp_fail time_atp)
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   372
        in log (sh_tag id ^ "failed: " ^ msg) end
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   373
    | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   374
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   375
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   376
end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   377
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   378
36499
7ec5ceef117b make Mirabelle happy
blanchet
parents: 36405
diff changeset
   379
val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
7ec5ceef117b make Mirabelle happy
blanchet
parents: 36405
diff changeset
   380
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   381
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   382
  let
37578
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents: 37577
diff changeset
   383
    open Metis_Clauses
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   384
    open Sledgehammer_Isar
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   385
    val thy = Proof.theory_of st
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   386
    val n0 = length (these (!named_thms))
36405
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   387
    val (prover_name, _) = get_atp thy args
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   388
    val timeout =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   389
      AList.lookup (op =) args minimize_timeoutK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   390
      |> Option.map (fst o read_int o explode)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   391
      |> the_default 5
36405
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   392
    val params = default_params thy
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   393
      [("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
37587
466031e057a0 compile
blanchet
parents: 37578
diff changeset
   394
    val minimize =
466031e057a0 compile
blanchet
parents: 37578
diff changeset
   395
      Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   396
    val _ = log separator
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   397
  in
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   398
    case minimize st (these (!named_thms)) of
35871
c93bda4fdf15 remove the iteration counter from Sledgehammer's minimizer
blanchet
parents: 35867
diff changeset
   399
      (SOME named_thms', msg) =>
32609
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
   400
        (change_data id inc_min_succs;
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
   401
         change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   402
         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
   403
         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
   404
         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
   405
               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
   406
        )
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   407
    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   408
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   409
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   410
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   411
fun run_metis full m name named_thms id
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   412
    ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   413
  let
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   414
    fun metis thms ctxt =
35830
d4c4f88f6432 fix Mirabelle after renaming Sledgehammer structures
blanchet
parents: 35592
diff changeset
   415
      if full then Metis_Tactics.metisFT_tac ctxt thms
d4c4f88f6432 fix Mirabelle after renaming Sledgehammer structures
blanchet
parents: 35592
diff changeset
   416
      else Metis_Tactics.metis_tac ctxt thms
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   417
    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   418
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   419
    fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   420
      | with_time (true, t) = (change_data id (inc_metis_success m);
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   421
          change_data id (inc_metis_lemmas m (length named_thms));
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   422
          change_data id (inc_metis_time m t);
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   423
          change_data id (inc_metis_posns m pos);
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   424
          if name = "proof" then change_data id (inc_metis_proofs m) else ();
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   425
          "succeeded (" ^ string_of_int t ^ ")")
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   426
    fun timed_metis thms =
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   427
      (with_time (Mirabelle.cpu_time apply_metis thms), true)
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   428
      handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m);
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   429
               ("timeout", false))
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   430
           | ERROR msg => ("error: " ^ msg, false)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   431
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   432
    val _ = log separator
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   433
    val _ = change_data id (inc_metis_calls m)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   434
  in
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   435
    maps snd named_thms
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   436
    |> timed_metis
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   437
    |>> log o prefix (metis_tag id)
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   438
    |> snd
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   439
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   440
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   441
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   442
  let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   443
    if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   444
    then () else
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   445
    let
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   446
      val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   447
      val minimize = AList.defined (op =) args minimizeK
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   448
      val metis_ft = AList.defined (op =) args metis_ftK
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   449
  
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   450
      fun apply_metis m1 m2 =
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   451
        if metis_ft
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   452
        then
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   453
          if not (Mirabelle.catch_result metis_tag false
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   454
              (run_metis false m1 name (these (!named_thms))) id st)
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   455
          then
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   456
            (Mirabelle.catch_result metis_tag false
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   457
              (run_metis true m2 name (these (!named_thms))) id st; ())
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   458
          else ()
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   459
        else
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   460
          (Mirabelle.catch_result metis_tag false
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   461
            (run_metis false m1 name (these (!named_thms))) id st; ())
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   462
    in 
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   463
      change_data id (set_mini minimize);
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   464
      Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   465
      if is_some (!named_thms)
32612
76dddd260d2f restructured code
nipkow
parents: 32609
diff changeset
   466
      then
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   467
       (apply_metis Unminimized UnminimizedFT;
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   468
        if minimize andalso not (null (these (!named_thms)))
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   469
        then
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   470
         (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   471
          apply_metis Minimized MinimizedFT)
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   472
        else ())
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   473
      else ()
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   474
    end
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   475
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   476
32511
43d2ac4aa2de added option full_typed for sledgehammer action
boehmes
parents: 32510
diff changeset
   477
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
   478
  let
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36294
diff changeset
   479
    val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   480
  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
   481
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   482
end