src/HOL/Tools/Sledgehammer/sledgehammer.ML
author blanchet
Mon Jun 02 17:34:26 2014 +0200 (2014-06-02 ago)
changeset 57158 f028d93798e6
parent 57101 c881a983a19f
child 57262 b2c629647a14
permissions -rw-r--r--
simplified counterexample handling
blanchet@55202
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer.ML
wenzelm@28477
     2
    Author:     Fabian Immler, TU Muenchen
wenzelm@32996
     3
    Author:     Makarius
blanchet@35969
     4
    Author:     Jasmin Blanchette, TU Muenchen
wenzelm@28477
     5
blanchet@38021
     6
Sledgehammer's heart.
wenzelm@28477
     7
*)
wenzelm@28477
     8
blanchet@55202
     9
signature SLEDGEHAMMER =
wenzelm@28477
    10
sig
blanchet@51008
    11
  type fact = Sledgehammer_Fact.fact
blanchet@48292
    12
  type fact_override = Sledgehammer_Fact.fact_override
blanchet@55287
    13
  type minimize_command = Sledgehammer_Proof_Methods.minimize_command
blanchet@55201
    14
  type mode = Sledgehammer_Prover.mode
blanchet@55201
    15
  type params = Sledgehammer_Prover.params
blanchet@40061
    16
blanchet@43020
    17
  val someN : string
blanchet@43020
    18
  val noneN : string
blanchet@43020
    19
  val timeoutN : string
blanchet@43020
    20
  val unknownN : string
blanchet@55212
    21
blanchet@51010
    22
  val string_of_factss : (string * fact list) list -> string
blanchet@54816
    23
  val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
blanchet@54816
    24
    ((string * string list) list -> string -> minimize_command) -> Proof.state ->
blanchet@54816
    25
    bool * (string * Proof.state)
wenzelm@28477
    26
end;
wenzelm@28477
    27
blanchet@55202
    28
structure Sledgehammer : SLEDGEHAMMER =
wenzelm@28477
    29
struct
wenzelm@28477
    30
blanchet@43085
    31
open ATP_Util
blanchet@55212
    32
open ATP_Proof
blanchet@46320
    33
open ATP_Problem_Generate
blanchet@38023
    34
open Sledgehammer_Util
blanchet@48250
    35
open Sledgehammer_Fact
blanchet@55287
    36
open Sledgehammer_Proof_Methods
blanchet@55201
    37
open Sledgehammer_Prover
blanchet@55212
    38
open Sledgehammer_Prover_ATP
blanchet@55202
    39
open Sledgehammer_Prover_Minimize
blanchet@48381
    40
open Sledgehammer_MaSh
blanchet@40072
    41
blanchet@43020
    42
val someN = "some"
blanchet@43020
    43
val noneN = "none"
blanchet@43020
    44
val timeoutN = "timeout"
blanchet@43020
    45
val unknownN = "unknown"
blanchet@43020
    46
blanchet@43020
    47
val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
blanchet@43020
    48
blanchet@43020
    49
fun max_outcome_code codes =
blanchet@43020
    50
  NONE
blanchet@43020
    51
  |> fold (fn candidate =>
blanchet@43020
    52
              fn accum as SOME _ => accum
blanchet@55286
    53
               | NONE => if member (op =) codes candidate then SOME candidate else NONE)
blanchet@55286
    54
       ordered_outcome_codes
blanchet@43020
    55
  |> the_default unknownN
blanchet@43020
    56
blanchet@57053
    57
fun prover_description verbose name num_facts =
blanchet@48319
    58
  (quote name,
blanchet@57053
    59
   if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "")
blanchet@41089
    60
blanchet@54816
    61
fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
blanchet@54816
    62
    output_result minimize_command only learn
blanchet@54816
    63
    {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
blanchet@41089
    64
  let
blanchet@41089
    65
    val ctxt = Proof.context_of state
blanchet@53800
    66
blanchet@54816
    67
    val hard_timeout = time_mult 3.0 timeout
blanchet@54062
    68
    val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
blanchet@41089
    69
    val birth_time = Time.now ()
blanchet@42850
    70
    val death_time = Time.+ (birth_time, hard_timeout)
blanchet@54126
    71
    val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
blanchet@48293
    72
    val num_facts = length facts |> not only ? Integer.min max_facts
blanchet@53800
    73
blanchet@41089
    74
    val problem =
blanchet@54141
    75
      {comment = comment, state = state, goal = goal, subgoal = subgoal,
blanchet@47904
    76
       subgoal_count = subgoal_count,
blanchet@53800
    77
       factss = factss
blanchet@51010
    78
         |> map (apsnd ((not (is_ho_atp ctxt name)
blanchet@51010
    79
                         ? filter_out (fn ((_, (_, Induction)), _) => true
blanchet@51010
    80
                                        | _ => false))
blanchet@51010
    81
                        #> take num_facts))}
blanchet@53800
    82
blanchet@51009
    83
    fun print_used_facts used_facts used_from =
blanchet@51009
    84
      tag_list 1 used_from
blanchet@51005
    85
      |> map (fn (j, fact) => fact |> apsnd (K j))
blanchet@48798
    86
      |> filter_used_facts false used_facts
blanchet@48394
    87
      |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
blanchet@48394
    88
      |> commas
blanchet@48394
    89
      |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
blanchet@48394
    90
                  " proof (of " ^ string_of_int (length facts) ^ "): ") "."
blanchet@48394
    91
      |> Output.urgent_message
blanchet@53800
    92
blanchet@54062
    93
    fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
blanchet@54062
    94
        let
blanchet@54062
    95
          val num_used_facts = length used_facts
blanchet@54063
    96
blanchet@54063
    97
          fun find_indices facts =
blanchet@54063
    98
            tag_list 1 facts
blanchet@54062
    99
            |> map (fn (j, fact) => fact |> apsnd (K j))
blanchet@54062
   100
            |> filter_used_facts false used_facts
blanchet@54773
   101
            |> distinct (eq_fst (op =))
blanchet@54062
   102
            |> map (prefix "@" o string_of_int o snd)
blanchet@54063
   103
blanchet@54063
   104
          fun filter_info (fact_filter, facts) =
blanchet@54063
   105
            let
blanchet@54063
   106
              val indices = find_indices facts
blanchet@54773
   107
              (* "Int.max" is there for robustness -- it shouldn't be necessary *)
blanchet@54773
   108
              val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?"
blanchet@54773
   109
            in
blanchet@54773
   110
              (commas (indices @ unknowns), fact_filter)
blanchet@54773
   111
            end
blanchet@54063
   112
blanchet@54063
   113
          val filter_infos =
blanchet@54063
   114
            map filter_info (("actual", used_from) :: factss)
blanchet@54063
   115
            |> AList.group (op =)
blanchet@54063
   116
            |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
blanchet@54062
   117
        in
blanchet@54063
   118
          "Success: Found proof with " ^ string_of_int num_used_facts ^
blanchet@54063
   119
          " of " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
blanchet@54063
   120
          (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
blanchet@53800
   121
        end
blanchet@53800
   122
      | spying_str_of_res {outcome = SOME failure, ...} =
blanchet@54062
   123
        "Failure: " ^ string_of_atp_failure failure
blanchet@53800
   124
blanchet@41255
   125
    fun really_go () =
blanchet@41263
   126
      problem
blanchet@51187
   127
      |> get_minimizing_prover ctxt mode learn name params minimize_command
blanchet@51009
   128
      |> verbose
blanchet@51009
   129
         ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
blanchet@51009
   130
                   print_used_facts used_facts used_from
blanchet@51009
   131
                 | _ => ())
blanchet@57056
   132
      |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
blanchet@43261
   133
      |> (fn {outcome, preplay, message, message_tail, ...} =>
blanchet@43005
   134
             (if outcome = SOME ATP_Proof.TimedOut then timeoutN
blanchet@43005
   135
              else if is_some outcome then noneN
blanchet@50669
   136
              else someN, fn () => message (Lazy.force preplay) ^ message_tail))
blanchet@53800
   137
blanchet@41089
   138
    fun go () =
blanchet@41089
   139
      let
blanchet@41089
   140
        val (outcome_code, message) =
blanchet@41089
   141
          if debug then
blanchet@41089
   142
            really_go ()
blanchet@41089
   143
          else
blanchet@41089
   144
            (really_go ()
blanchet@57056
   145
             handle
blanchet@57056
   146
               ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
blanchet@57056
   147
             | exn =>
blanchet@57056
   148
               if Exn.is_interrupt exn then reraise exn
blanchet@57056
   149
               else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
blanchet@57056
   150
blanchet@41089
   151
        val _ =
blanchet@41142
   152
          (* The "expect" argument is deliberately ignored if the prover is
blanchet@41142
   153
             missing so that the "Metis_Examples" can be processed on any
blanchet@41142
   154
             machine. *)
blanchet@41142
   155
          if expect = "" orelse outcome_code = expect orelse
blanchet@41142
   156
             not (is_prover_installed ctxt name) then
blanchet@41089
   157
            ()
blanchet@41089
   158
          else if blocking then
blanchet@41089
   159
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
blanchet@41089
   160
          else
blanchet@41089
   161
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
blanchet@43005
   162
      in (outcome_code, message) end
blanchet@41089
   163
  in
blanchet@43021
   164
    if mode = Auto_Try then
blanchet@54816
   165
      let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
blanchet@43006
   166
        (outcome_code,
blanchet@43006
   167
         state
blanchet@43006
   168
         |> outcome_code = someN
blanchet@43006
   169
            ? Proof.goal_message (fn () =>
wenzelm@52643
   170
                  Pretty.mark Markup.information (Pretty.str (message ()))))
blanchet@41089
   171
      end
blanchet@41089
   172
    else if blocking then
blanchet@43006
   173
      let
blanchet@43006
   174
        val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
wenzelm@53048
   175
        val outcome =
blanchet@57056
   176
          if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
wenzelm@53048
   177
        val _ =
wenzelm@53052
   178
          if outcome <> "" andalso is_some output_result then
wenzelm@53048
   179
            the output_result outcome
wenzelm@52908
   180
          else
wenzelm@53048
   181
            outcome
wenzelm@53048
   182
            |> Async_Manager.break_into_chunks
wenzelm@53048
   183
            |> List.app Output.urgent_message
wenzelm@53048
   184
      in (outcome_code, state) end
blanchet@41089
   185
    else
blanchet@57053
   186
      (Async_Manager.thread SledgehammerN birth_time death_time
blanchet@57053
   187
         (prover_description verbose name num_facts)
blanchet@55212
   188
         ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
blanchet@43006
   189
       (unknownN, state))
blanchet@41089
   190
  end
blanchet@41089
   191
blanchet@48293
   192
val auto_try_max_facts_divisor = 2 (* FUDGE *)
blanchet@40060
   193
blanchet@51008
   194
fun string_of_facts facts =
blanchet@57101
   195
  "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
blanchet@51008
   196
  (facts |> map (fst o fst) |> space_implode " ") ^ "."
blanchet@51008
   197
blanchet@51010
   198
fun string_of_factss factss =
blanchet@51010
   199
  if forall (null o snd) factss then
blanchet@51010
   200
    "Found no relevant facts."
blanchet@55286
   201
  else
blanchet@55286
   202
    (case factss of
blanchet@55286
   203
      [(_, facts)] => string_of_facts facts
blanchet@55286
   204
    | _ =>
blanchet@55286
   205
      factss
blanchet@55286
   206
      |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
blanchet@55286
   207
      |> space_implode "\n\n")
blanchet@51008
   208
blanchet@54799
   209
fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode
blanchet@54799
   210
    output_result i (fact_override as {only, ...}) minimize_command state =
blanchet@40059
   211
  if null provers then
blanchet@40059
   212
    error "No prover is set."
blanchet@55286
   213
  else
blanchet@55286
   214
    (case subgoal_count state of
blanchet@55286
   215
      0 =>
wenzelm@52908
   216
      ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
blanchet@55286
   217
    | n =>
blanchet@55286
   218
      let
blanchet@55286
   219
        val _ = Proof.assert_backward state
blanchet@55286
   220
        val print =
blanchet@55286
   221
          if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
blanchet@55286
   222
        val ctxt = Proof.context_of state
blanchet@55286
   223
        val {facts = chained, goal, ...} = Proof.goal state
blanchet@55286
   224
        val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
blanchet@55286
   225
        val ho_atp = exists (is_ho_atp ctxt) provers
blanchet@55286
   226
        val reserved = reserved_isar_keyword_table ()
blanchet@55286
   227
        val css = clasimpset_rule_table_of ctxt
blanchet@55286
   228
        val all_facts =
blanchet@55286
   229
          nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
blanchet@55286
   230
                           concl_t
blanchet@55286
   231
        val _ = () |> not blocking ? kill_provers
blanchet@55286
   232
        val _ =
blanchet@55286
   233
          (case find_first (not o is_prover_supported ctxt) provers of
blanchet@55286
   234
            SOME name => error ("No such prover: " ^ name ^ ".")
blanchet@55286
   235
          | NONE => ())
blanchet@55286
   236
        val _ = print "Sledgehammering..."
blanchet@57037
   237
        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
blanchet@54090
   238
blanchet@55286
   239
        val spying_str_of_factss =
blanchet@55286
   240
          commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
blanchet@53800
   241
blanchet@55286
   242
        fun get_factss provers =
blanchet@55286
   243
          let
blanchet@55286
   244
            val max_max_facts =
blanchet@55286
   245
              (case max_facts of
blanchet@55286
   246
                SOME n => n
blanchet@55286
   247
              | NONE =>
blanchet@55286
   248
                0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
blanchet@55286
   249
                  |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
blanchet@55286
   250
            val _ = spying spy (fn () => (state, i, "All",
blanchet@55286
   251
              "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
blanchet@55286
   252
          in
blanchet@55286
   253
            all_facts
blanchet@55286
   254
            |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
blanchet@55286
   255
            |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
blanchet@55286
   256
            |> spy ? tap (fn factss => spying spy (fn () =>
blanchet@55286
   257
              (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
blanchet@55286
   258
          end
blanchet@53800
   259
blanchet@55286
   260
        fun launch_provers state =
blanchet@55286
   261
          let
blanchet@55286
   262
            val factss = get_factss provers
blanchet@55286
   263
            val problem =
blanchet@55286
   264
              {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@55286
   265
               factss = factss}
blanchet@55286
   266
            val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
blanchet@55286
   267
            val launch = launch_prover params mode output_result minimize_command only learn
blanchet@55286
   268
          in
blanchet@55286
   269
            if mode = Auto_Try then
blanchet@55286
   270
              (unknownN, state)
blanchet@55286
   271
              |> fold (fn prover => fn accum as (outcome_code, _) =>
blanchet@57056
   272
                  if outcome_code = someN then accum else launch problem prover)
blanchet@57056
   273
                provers
blanchet@55286
   274
            else
blanchet@55286
   275
              provers
blanchet@55286
   276
              |> (if blocking then Par_List.map else map) (launch problem #> fst)
blanchet@55286
   277
              |> max_outcome_code |> rpair state
blanchet@55286
   278
          end
blanchet@55286
   279
      in
blanchet@55286
   280
        (if blocking then launch_provers state
blanchet@55286
   281
         else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
blanchet@55286
   282
        handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
blanchet@55286
   283
      end
blanchet@55286
   284
      |> `(fn (outcome_code, _) => outcome_code = someN))
blanchet@38044
   285
wenzelm@28582
   286
end;