src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 54546 8b403a7a8c44
parent 54503 b490e15a5e19
child 54773 79f66cd15d57
permissions -rw-r--r--
fixed spying so that the envirnoment variables are queried at run-time not at build-time
blanchet@41087
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_run.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@41087
     9
signature SLEDGEHAMMER_RUN =
wenzelm@28477
    10
sig
blanchet@51008
    11
  type fact = Sledgehammer_Fact.fact
blanchet@48292
    12
  type fact_override = Sledgehammer_Fact.fact_override
smolkas@52555
    13
  type minimize_command = Sledgehammer_Reconstructor.minimize_command
blanchet@43021
    14
  type mode = Sledgehammer_Provers.mode
blanchet@41087
    15
  type params = Sledgehammer_Provers.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@51010
    21
  val string_of_factss : (string * fact list) list -> string
blanchet@38044
    22
  val run_sledgehammer :
wenzelm@53048
    23
    params -> mode -> (string -> unit) option -> int -> fact_override
blanchet@45520
    24
    -> ((string * string list) list -> string -> minimize_command)
blanchet@43020
    25
    -> Proof.state -> bool * (string * Proof.state)
wenzelm@28477
    26
end;
wenzelm@28477
    27
blanchet@41087
    28
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
wenzelm@28477
    29
struct
wenzelm@28477
    30
blanchet@43085
    31
open ATP_Util
blanchet@46320
    32
open ATP_Problem_Generate
blanchet@53800
    33
open ATP_Proof
blanchet@46320
    34
open ATP_Proof_Reconstruct
blanchet@38023
    35
open Sledgehammer_Util
blanchet@48250
    36
open Sledgehammer_Fact
blanchet@41087
    37
open Sledgehammer_Provers
blanchet@41091
    38
open Sledgehammer_Minimize
blanchet@48381
    39
open Sledgehammer_MaSh
blanchet@40072
    40
blanchet@43020
    41
val someN = "some"
blanchet@43020
    42
val noneN = "none"
blanchet@43020
    43
val timeoutN = "timeout"
blanchet@43020
    44
val unknownN = "unknown"
blanchet@43020
    45
blanchet@43020
    46
val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
blanchet@43020
    47
blanchet@43020
    48
fun max_outcome_code codes =
blanchet@43020
    49
  NONE
blanchet@43020
    50
  |> fold (fn candidate =>
blanchet@43020
    51
              fn accum as SOME _ => accum
blanchet@43020
    52
               | NONE => if member (op =) codes candidate then SOME candidate
blanchet@43020
    53
                         else NONE)
blanchet@43020
    54
          ordered_outcome_codes
blanchet@43020
    55
  |> the_default unknownN
blanchet@43020
    56
blanchet@41208
    57
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
blanchet@41089
    58
                       n goal =
blanchet@48319
    59
  (quote name,
blanchet@43005
    60
   (if verbose then
blanchet@43005
    61
      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
blanchet@43005
    62
    else
blanchet@43005
    63
      "") ^
blanchet@43005
    64
   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
blanchet@45379
    65
   (if blocking then "."
blanchet@45379
    66
    else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
blanchet@41089
    67
blanchet@53800
    68
fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, slice,
blanchet@43059
    69
                              timeout, expect, ...})
wenzelm@53048
    70
        mode output_result minimize_command only learn
blanchet@54141
    71
        {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
blanchet@41089
    72
  let
blanchet@41089
    73
    val ctxt = Proof.context_of state
blanchet@53800
    74
blanchet@50749
    75
    val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
blanchet@54062
    76
    val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
blanchet@41089
    77
    val birth_time = Time.now ()
blanchet@42850
    78
    val death_time = Time.+ (birth_time, hard_timeout)
blanchet@54126
    79
    val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
blanchet@48293
    80
    val num_facts = length facts |> not only ? Integer.min max_facts
blanchet@53800
    81
blanchet@53800
    82
    fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
blanchet@53800
    83
blanchet@41089
    84
    val problem =
blanchet@54141
    85
      {comment = comment, state = state, goal = goal, subgoal = subgoal,
blanchet@47904
    86
       subgoal_count = subgoal_count,
blanchet@53800
    87
       factss = factss
blanchet@51010
    88
         |> map (apsnd ((not (is_ho_atp ctxt name)
blanchet@51010
    89
                         ? filter_out (fn ((_, (_, Induction)), _) => true
blanchet@51010
    90
                                        | _ => false))
blanchet@51010
    91
                        #> take num_facts))}
blanchet@53800
    92
blanchet@51009
    93
    fun print_used_facts used_facts used_from =
blanchet@51009
    94
      tag_list 1 used_from
blanchet@51005
    95
      |> map (fn (j, fact) => fact |> apsnd (K j))
blanchet@48798
    96
      |> filter_used_facts false used_facts
blanchet@48394
    97
      |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
blanchet@48394
    98
      |> commas
blanchet@48394
    99
      |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
blanchet@48394
   100
                  " proof (of " ^ string_of_int (length facts) ^ "): ") "."
blanchet@48394
   101
      |> Output.urgent_message
blanchet@53800
   102
blanchet@54062
   103
    fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
blanchet@54062
   104
        let
blanchet@54062
   105
          val num_used_facts = length used_facts
blanchet@54063
   106
blanchet@54063
   107
          fun find_indices facts =
blanchet@54063
   108
            tag_list 1 facts
blanchet@54062
   109
            |> map (fn (j, fact) => fact |> apsnd (K j))
blanchet@54062
   110
            |> filter_used_facts false used_facts
blanchet@54062
   111
            |> map (prefix "@" o string_of_int o snd)
blanchet@54063
   112
blanchet@54063
   113
          fun filter_info (fact_filter, facts) =
blanchet@54063
   114
            let
blanchet@54063
   115
              val indices = find_indices facts
blanchet@54063
   116
              val unknowns = replicate (num_used_facts - length indices) "?"
blanchet@54063
   117
            in (commas (indices @ unknowns), fact_filter) end
blanchet@54063
   118
blanchet@54063
   119
          val filter_infos =
blanchet@54063
   120
            map filter_info (("actual", used_from) :: factss)
blanchet@54063
   121
            |> AList.group (op =)
blanchet@54063
   122
            |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
blanchet@54062
   123
        in
blanchet@54063
   124
          "Success: Found proof with " ^ string_of_int num_used_facts ^
blanchet@54063
   125
          " of " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
blanchet@54063
   126
          (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
blanchet@53800
   127
        end
blanchet@53800
   128
      | spying_str_of_res {outcome = SOME failure, ...} =
blanchet@54062
   129
        "Failure: " ^ string_of_atp_failure failure
blanchet@53800
   130
blanchet@41255
   131
    fun really_go () =
blanchet@41263
   132
      problem
blanchet@51187
   133
      |> get_minimizing_prover ctxt mode learn name params minimize_command
blanchet@51009
   134
      |> verbose
blanchet@51009
   135
         ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
blanchet@51009
   136
                   print_used_facts used_facts used_from
blanchet@51009
   137
                 | _ => ())
blanchet@53800
   138
      |> spy
blanchet@53815
   139
         ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
blanchet@43261
   140
      |> (fn {outcome, preplay, message, message_tail, ...} =>
blanchet@43005
   141
             (if outcome = SOME ATP_Proof.TimedOut then timeoutN
blanchet@43005
   142
              else if is_some outcome then noneN
blanchet@50669
   143
              else someN, fn () => message (Lazy.force preplay) ^ message_tail))
blanchet@53800
   144
blanchet@41089
   145
    fun go () =
blanchet@41089
   146
      let
blanchet@41089
   147
        val (outcome_code, message) =
blanchet@41089
   148
          if debug then
blanchet@41089
   149
            really_go ()
blanchet@41089
   150
          else
blanchet@41089
   151
            (really_go ()
blanchet@43052
   152
             handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
blanchet@41089
   153
                  | exn =>
blanchet@41089
   154
                    if Exn.is_interrupt exn then
blanchet@41089
   155
                      reraise exn
blanchet@41089
   156
                    else
blanchet@43052
   157
                      (unknownN, fn () => "Internal error:\n" ^
blanchet@43052
   158
                                          ML_Compiler.exn_message exn ^ "\n"))
blanchet@41089
   159
        val _ =
blanchet@41142
   160
          (* The "expect" argument is deliberately ignored if the prover is
blanchet@41142
   161
             missing so that the "Metis_Examples" can be processed on any
blanchet@41142
   162
             machine. *)
blanchet@41142
   163
          if expect = "" orelse outcome_code = expect orelse
blanchet@41142
   164
             not (is_prover_installed ctxt name) then
blanchet@41089
   165
            ()
blanchet@41089
   166
          else if blocking then
blanchet@41089
   167
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
blanchet@41089
   168
          else
blanchet@41089
   169
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
blanchet@43005
   170
      in (outcome_code, message) end
blanchet@41089
   171
  in
blanchet@43021
   172
    if mode = Auto_Try then
blanchet@50557
   173
      let val (outcome_code, message) = time_limit timeout go () in
blanchet@43006
   174
        (outcome_code,
blanchet@43006
   175
         state
blanchet@43006
   176
         |> outcome_code = someN
blanchet@43006
   177
            ? Proof.goal_message (fn () =>
wenzelm@52643
   178
                  Pretty.mark Markup.information (Pretty.str (message ()))))
blanchet@41089
   179
      end
blanchet@41089
   180
    else if blocking then
blanchet@43006
   181
      let
blanchet@43006
   182
        val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
wenzelm@53048
   183
        val outcome =
wenzelm@53052
   184
          if outcome_code = someN orelse mode = Normal then
wenzelm@53048
   185
            quote name ^ ": " ^ message ()
wenzelm@53048
   186
          else ""
wenzelm@53048
   187
        val _ =
wenzelm@53052
   188
          if outcome <> "" andalso is_some output_result then
wenzelm@53048
   189
            the output_result outcome
wenzelm@52908
   190
          else
wenzelm@53048
   191
            outcome
wenzelm@53048
   192
            |> Async_Manager.break_into_chunks
wenzelm@53048
   193
            |> List.app Output.urgent_message
wenzelm@53048
   194
      in (outcome_code, state) end
blanchet@41089
   195
    else
wenzelm@52048
   196
      (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
blanchet@43052
   197
                            ((fn (outcome_code, message) =>
blanchet@43059
   198
                                 (verbose orelse outcome_code = someN,
blanchet@43059
   199
                                  message ())) o go);
blanchet@43006
   200
       (unknownN, state))
blanchet@41089
   201
  end
blanchet@41089
   202
blanchet@48293
   203
val auto_try_max_facts_divisor = 2 (* FUDGE *)
blanchet@40060
   204
blanchet@51008
   205
fun string_of_facts facts =
blanchet@51008
   206
  "Including " ^ string_of_int (length facts) ^
blanchet@51008
   207
  " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
blanchet@51008
   208
  (facts |> map (fst o fst) |> space_implode " ") ^ "."
blanchet@51008
   209
blanchet@51010
   210
fun string_of_factss factss =
blanchet@51010
   211
  if forall (null o snd) factss then
blanchet@51010
   212
    "Found no relevant facts."
blanchet@51010
   213
  else case factss of
blanchet@51010
   214
    [(_, facts)] => string_of_facts facts
blanchet@51010
   215
  | _ =>
blanchet@51010
   216
    factss
blanchet@51010
   217
    |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
blanchet@51010
   218
    |> space_implode "\n\n"
blanchet@51008
   219
blanchet@53800
   220
fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, slice, ...})
wenzelm@53048
   221
        mode output_result i (fact_override as {only, ...}) minimize_command state =
blanchet@40059
   222
  if null provers then
blanchet@40059
   223
    error "No prover is set."
blanchet@39318
   224
  else case subgoal_count state of
wenzelm@52908
   225
    0 =>
wenzelm@52908
   226
      ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
blanchet@39318
   227
  | n =>
blanchet@39318
   228
    let
blanchet@39364
   229
      val _ = Proof.assert_backward state
wenzelm@53052
   230
      val print =
wenzelm@53052
   231
        if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
blanchet@54090
   232
      val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug)
blanchet@40200
   233
      val ctxt = Proof.context_of state
blanchet@48396
   234
      val {facts = chained, goal, ...} = Proof.goal state
blanchet@52196
   235
      val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
blanchet@51007
   236
      val ho_atp = exists (is_ho_atp ctxt) provers
blanchet@48299
   237
      val reserved = reserved_isar_keyword_table ()
blanchet@48396
   238
      val css = clasimpset_rule_table_of ctxt
blanchet@48407
   239
      val all_facts =
blanchet@48396
   240
        nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
blanchet@48396
   241
                         concl_t
nik@44586
   242
      val _ = () |> not blocking ? kill_provers
blanchet@41727
   243
      val _ = case find_first (not o is_prover_supported ctxt) provers of
blanchet@40941
   244
                SOME name => error ("No such prover: " ^ name ^ ".")
blanchet@40941
   245
              | NONE => ()
blanchet@41773
   246
      val _ = print "Sledgehammering..."
blanchet@54090
   247
      val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
blanchet@54090
   248
blanchet@54090
   249
      val (ueq_atps, full_provers) = List.partition (is_unit_equational_atp ctxt) provers
blanchet@53800
   250
blanchet@53800
   251
      val spying_str_of_factss =
blanchet@53800
   252
        commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
blanchet@53800
   253
blanchet@51010
   254
      fun get_factss label is_appropriate_prop provers =
blanchet@41242
   255
        let
blanchet@48293
   256
          val max_max_facts =
blanchet@48293
   257
            case max_facts of
blanchet@41242
   258
              SOME n => n
blanchet@41242
   259
            | NONE =>
blanchet@54126
   260
              0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
blanchet@48293
   261
                |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
blanchet@53815
   262
          val _ = spying spy (fn () => (state, i, label ^ "s",
blanchet@54063
   263
            "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
blanchet@41242
   264
        in
blanchet@48407
   265
          all_facts
blanchet@43351
   266
          |> (case is_appropriate_prop of
blanchet@43351
   267
                SOME is_app => filter (is_app o prop_of o snd)
blanchet@43351
   268
              | NONE => I)
blanchet@54062
   269
          |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
blanchet@51010
   270
          |> tap (fn factss =>
blanchet@48394
   271
                     if verbose then
blanchet@41242
   272
                       label ^ plural_s (length provers) ^ ": " ^
blanchet@51010
   273
                       string_of_factss factss
blanchet@41773
   274
                       |> print
blanchet@41242
   275
                     else
blanchet@41242
   276
                       ())
blanchet@54062
   277
          |> spy ? tap (fn factss => spying spy (fn () =>
blanchet@54062
   278
            (state, i, label ^ "s", "Selected facts: " ^ spying_str_of_factss factss)))
blanchet@41242
   279
        end
blanchet@53800
   280
blanchet@51006
   281
      fun launch_provers state label is_appropriate_prop provers =
blanchet@51006
   282
        let
blanchet@51010
   283
          val factss = get_factss label is_appropriate_prop provers
blanchet@51006
   284
          val problem =
blanchet@54141
   285
            {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@51010
   286
             factss = factss}
blanchet@54503
   287
          val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
blanchet@54503
   288
          val launch = launch_prover params mode output_result minimize_command only learn
blanchet@51006
   289
        in
wenzelm@53048
   290
          if mode = Auto_Try then
blanchet@51006
   291
            (unknownN, state)
blanchet@51006
   292
            |> fold (fn prover => fn accum as (outcome_code, _) =>
blanchet@51006
   293
                        if outcome_code = someN then accum
blanchet@51006
   294
                        else launch problem prover)
blanchet@51006
   295
                    provers
blanchet@51006
   296
          else
blanchet@51006
   297
            provers
blanchet@51006
   298
            |> (if blocking then Par_List.map else map) (launch problem #> fst)
blanchet@51006
   299
            |> max_outcome_code |> rpair state
blanchet@51006
   300
        end
blanchet@53800
   301
blanchet@54090
   302
      fun maybe_launch_provers label is_appropriate_prop provers_to_launch accum =
blanchet@54090
   303
        if null provers_to_launch then
blanchet@41256
   304
          accum
blanchet@43351
   305
        else if is_some is_appropriate_prop andalso
blanchet@43351
   306
                not (the is_appropriate_prop concl_t) then
blanchet@54090
   307
          (if verbose orelse length provers_to_launch = length provers then
blanchet@42946
   308
             "Goal outside the scope of " ^
blanchet@54090
   309
             space_implode " " (serial_commas "and" (map quote provers_to_launch)) ^ "."
blanchet@42946
   310
             |> Output.urgent_message
blanchet@42946
   311
           else
blanchet@42946
   312
             ();
blanchet@42946
   313
           accum)
blanchet@41256
   314
        else
blanchet@54090
   315
          launch_provers state label is_appropriate_prop provers_to_launch
blanchet@53800
   316
blanchet@54090
   317
      val launch_full_provers = maybe_launch_provers "ATP/SMT" NONE full_provers
blanchet@54090
   318
      val launch_ueq_atps = maybe_launch_provers "Unit-equational provers" (SOME is_unit_equality) ueq_atps
blanchet@53800
   319
blanchet@54057
   320
      fun launch_atps_and_smt_solvers p =
blanchet@54090
   321
        [launch_full_provers, launch_ueq_atps]
blanchet@54057
   322
        |> Par_List.map (fn f => fst (f p))
blanchet@41773
   323
        handle ERROR msg => (print ("Error: " ^ msg); error msg)
blanchet@53800
   324
blanchet@43021
   325
      fun maybe f (accum as (outcome_code, _)) =
wenzelm@53052
   326
        accum |> (mode = Normal orelse outcome_code <> someN) ? f
blanchet@40060
   327
    in
blanchet@43020
   328
      (unknownN, state)
blanchet@54090
   329
      |> (if blocking then launch_full_provers
blanchet@54090
   330
          else (fn p => (Future.fork (tap (fn () => launch_full_provers p)); p)))
blanchet@54090
   331
      handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
blanchet@40060
   332
    end
blanchet@43020
   333
    |> `(fn (outcome_code, _) => outcome_code = someN)
blanchet@38044
   334
wenzelm@28582
   335
end;