src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Wed Dec 15 11:26:28 2010 +0100 (2010-12-15 ago)
changeset 41142 43e2b051339c
parent 41138 eb80538166b6
child 41171 043f8dc3b51f
permissions -rw-r--r--
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
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@38988
    11
  type relevance_override = Sledgehammer_Filter.relevance_override
blanchet@40068
    12
  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
blanchet@41087
    13
  type params = Sledgehammer_Provers.params
blanchet@40061
    14
blanchet@38044
    15
  val run_sledgehammer :
blanchet@39318
    16
    params -> bool -> int -> relevance_override -> (string -> minimize_command)
blanchet@39318
    17
    -> Proof.state -> bool * Proof.state
wenzelm@28477
    18
end;
wenzelm@28477
    19
blanchet@41087
    20
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
wenzelm@28477
    21
struct
wenzelm@28477
    22
blanchet@38023
    23
open Sledgehammer_Util
blanchet@38988
    24
open Sledgehammer_Filter
blanchet@40068
    25
open Sledgehammer_ATP_Translate
blanchet@41087
    26
open Sledgehammer_Provers
blanchet@41091
    27
open Sledgehammer_Minimize
blanchet@40072
    28
blanchet@41089
    29
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
blanchet@41089
    30
                       n goal =
blanchet@41089
    31
  quote name ^
blanchet@41089
    32
  (if verbose then
blanchet@41089
    33
     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
blanchet@41089
    34
   else
blanchet@41089
    35
     "") ^
blanchet@41089
    36
  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
blanchet@41089
    37
  (if blocking then
blanchet@41089
    38
     ""
blanchet@41089
    39
   else
blanchet@41089
    40
     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
blanchet@41089
    41
blanchet@41091
    42
val implicit_minimization_threshold = 50
blanchet@41091
    43
blanchet@41089
    44
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
blanchet@41089
    45
               auto minimize_command only
blanchet@41089
    46
               {state, goal, subgoal, subgoal_count, facts} name =
blanchet@41089
    47
  let
blanchet@41089
    48
    val ctxt = Proof.context_of state
blanchet@41089
    49
    val birth_time = Time.now ()
blanchet@41089
    50
    val death_time = Time.+ (birth_time, timeout)
blanchet@41089
    51
    val max_relevant =
blanchet@41089
    52
      the_default (default_max_relevant_for_prover ctxt name) max_relevant
blanchet@41089
    53
    val num_facts = length facts |> not only ? Integer.min max_relevant
blanchet@41089
    54
    val desc =
blanchet@41089
    55
      prover_description ctxt params name num_facts subgoal subgoal_count goal
blanchet@41089
    56
    val prover = get_prover ctxt auto name
blanchet@41089
    57
    val problem =
blanchet@41089
    58
      {state = state, goal = goal, subgoal = subgoal,
blanchet@41089
    59
       subgoal_count = subgoal_count, facts = take num_facts facts}
blanchet@41089
    60
    fun go () =
blanchet@41089
    61
      let
blanchet@41089
    62
        fun really_go () =
blanchet@41089
    63
          prover params (minimize_command name) problem
blanchet@41091
    64
          |> (fn {outcome, used_facts, message, ...} =>
blanchet@41091
    65
                 if is_some outcome then
blanchet@41091
    66
                   ("none", message)
blanchet@41091
    67
                 else
blanchet@41091
    68
                   ("some",
blanchet@41091
    69
                    if length used_facts >= implicit_minimization_threshold then
blanchet@41091
    70
                      minimize_facts params true subgoal subgoal_count state
blanchet@41091
    71
                          (filter_used_facts used_facts
blanchet@41091
    72
                               (map (apsnd single o untranslated_fact) facts))
blanchet@41091
    73
                      |> snd
blanchet@41091
    74
                    else
blanchet@41091
    75
                      message))
blanchet@41089
    76
        val (outcome_code, message) =
blanchet@41089
    77
          if debug then
blanchet@41089
    78
            really_go ()
blanchet@41089
    79
          else
blanchet@41089
    80
            (really_go ()
blanchet@41089
    81
             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
blanchet@41089
    82
                  | exn =>
blanchet@41089
    83
                    if Exn.is_interrupt exn then
blanchet@41089
    84
                      reraise exn
blanchet@41089
    85
                    else
blanchet@41089
    86
                      ("unknown", "Internal error:\n" ^
blanchet@41089
    87
                                  ML_Compiler.exn_message exn ^ "\n"))
blanchet@41089
    88
        val _ =
blanchet@41142
    89
          (* The "expect" argument is deliberately ignored if the prover is
blanchet@41142
    90
             missing so that the "Metis_Examples" can be processed on any
blanchet@41142
    91
             machine. *)
blanchet@41142
    92
          if expect = "" orelse outcome_code = expect orelse
blanchet@41142
    93
             not (is_prover_installed ctxt name) then
blanchet@41089
    94
            ()
blanchet@41089
    95
          else if blocking then
blanchet@41089
    96
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
blanchet@41089
    97
          else
blanchet@41089
    98
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
blanchet@41089
    99
      in (outcome_code = "some", message) end
blanchet@41089
   100
  in
blanchet@41089
   101
    if auto then
blanchet@41089
   102
      let val (success, message) = TimeLimit.timeLimit timeout go () in
blanchet@41089
   103
        (success, state |> success ? Proof.goal_message (fn () =>
blanchet@41091
   104
             Pretty.chunks [Pretty.str "",
blanchet@41091
   105
                            Pretty.mark Markup.hilite (Pretty.str message)]))
blanchet@41089
   106
      end
blanchet@41089
   107
    else if blocking then
blanchet@41089
   108
      let val (success, message) = TimeLimit.timeLimit timeout go () in
blanchet@41089
   109
        List.app Output.urgent_message
blanchet@41089
   110
                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
blanchet@41089
   111
        (success, state)
blanchet@41089
   112
      end
blanchet@41089
   113
    else
blanchet@41089
   114
      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
blanchet@41089
   115
       (false, state))
blanchet@41089
   116
  end
blanchet@41089
   117
blanchet@40698
   118
(* FUDGE *)
blanchet@40698
   119
val auto_max_relevant_divisor = 2
blanchet@40060
   120
blanchet@41138
   121
fun run_sledgehammer (params as {blocking, debug, provers, type_sys,
blanchet@40069
   122
                                 relevance_thresholds, max_relevant, ...})
blanchet@39366
   123
                     auto i (relevance_override as {only, ...}) minimize_command
blanchet@39366
   124
                     state =
blanchet@40059
   125
  if null provers then
blanchet@40059
   126
    error "No prover is set."
blanchet@39318
   127
  else case subgoal_count state of
wenzelm@40132
   128
    0 => (Output.urgent_message "No subgoal!"; (false, state))
blanchet@39318
   129
  | n =>
blanchet@39318
   130
    let
blanchet@39364
   131
      val _ = Proof.assert_backward state
blanchet@40200
   132
      val ctxt = Proof.context_of state
blanchet@40200
   133
      val {facts = chained_ths, goal, ...} = Proof.goal state
blanchet@40060
   134
      val (_, hyp_ts, concl_t) = strip_subgoal goal i
blanchet@41138
   135
      val no_dangerous_types = types_dangerous_types type_sys
blanchet@40059
   136
      val _ = () |> not blocking ? kill_provers
blanchet@40941
   137
      val _ = case find_first (not o is_prover_available ctxt) provers of
blanchet@40941
   138
                SOME name => error ("No such prover: " ^ name ^ ".")
blanchet@40941
   139
              | NONE => ()
wenzelm@40132
   140
      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
blanchet@40941
   141
      val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
blanchet@41138
   142
      fun run_provers label no_dangerous_types relevance_fudge maybe_translate
blanchet@41138
   143
                      provers (res as (success, state)) =
blanchet@40065
   144
        if success orelse null provers then
blanchet@40060
   145
          res
blanchet@40060
   146
        else
blanchet@40060
   147
          let
blanchet@40060
   148
            val max_max_relevant =
blanchet@40060
   149
              case max_relevant of
blanchet@40060
   150
                SOME n => n
blanchet@40060
   151
              | NONE =>
blanchet@40941
   152
                0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
blanchet@40065
   153
                          provers
blanchet@40060
   154
                  |> auto ? (fn n => n div auto_max_relevant_divisor)
blanchet@40369
   155
            val is_built_in_const =
blanchet@40369
   156
              is_built_in_const_for_prover ctxt (hd provers)
blanchet@40204
   157
            val facts =
blanchet@41138
   158
              relevant_facts ctxt no_dangerous_types relevance_thresholds
blanchet@40369
   159
                             max_max_relevant is_built_in_const relevance_fudge
blanchet@40071
   160
                             relevance_override chained_ths hyp_ts concl_t
blanchet@40114
   161
              |> map maybe_translate
blanchet@40062
   162
            val problem =
blanchet@40065
   163
              {state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@40983
   164
               facts = facts}
blanchet@40983
   165
            val run_prover = run_prover params auto minimize_command only
blanchet@40060
   166
          in
blanchet@40205
   167
            if debug then
blanchet@40370
   168
              Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
blanchet@40205
   169
                  (if null facts then
blanchet@40205
   170
                     "Found no relevant facts."
blanchet@40205
   171
                   else
blanchet@40205
   172
                     "Including (up to) " ^ string_of_int (length facts) ^
blanchet@40205
   173
                     " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
blanchet@41091
   174
                     (facts |> map (fst o fst o untranslated_fact)
blanchet@40205
   175
                            |> space_implode " ") ^ "."))
blanchet@40205
   176
            else
blanchet@40205
   177
              ();
blanchet@40060
   178
            if auto then
blanchet@40061
   179
              fold (fn prover => fn (true, state) => (true, state)
blanchet@40064
   180
                                  | (false, _) => run_prover problem prover)
blanchet@40065
   181
                   provers (false, state)
blanchet@40060
   182
            else
blanchet@40065
   183
              provers |> (if blocking then Par_List.map else map)
blanchet@40065
   184
                             (run_prover problem)
blanchet@40065
   185
                      |> exists fst |> rpair state
blanchet@40060
   186
          end
blanchet@40071
   187
      val run_atps =
blanchet@41138
   188
        run_provers "ATP" no_dangerous_types atp_relevance_fudge
blanchet@41090
   189
                    (ATP_Translated_Fact o translate_atp_fact ctxt) atps
blanchet@40071
   190
      val run_smts =
blanchet@41090
   191
        run_provers "SMT solver" true smt_relevance_fudge Untranslated_Fact smts
blanchet@40060
   192
      fun run_atps_and_smt_solvers () =
blanchet@40065
   193
        [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
blanchet@40060
   194
    in
blanchet@40065
   195
      (false, state)
blanchet@40065
   196
      |> (if blocking then run_atps #> not auto ? run_smts
blanchet@40065
   197
          else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
blanchet@40060
   198
    end
blanchet@38044
   199
wenzelm@28582
   200
end;