src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Wed Dec 08 22:17:52 2010 +0100 (2010-12-08 ago)
changeset 41087 d7b5fd465198
parent 41066 src/HOL/Tools/Sledgehammer/sledgehammer.ML@3890ef4e02f9
child 41088 54eb8e7c7f9b
permissions -rw-r--r--
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
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@40072
    27
blanchet@40698
    28
(* FUDGE *)
blanchet@40698
    29
val auto_max_relevant_divisor = 2
blanchet@40060
    30
blanchet@40205
    31
fun fact_name (Untranslated ((name, _), _)) = SOME name
blanchet@40205
    32
  | fact_name (Translated (_, p)) = Option.map (fst o fst) p
blanchet@40061
    33
blanchet@40205
    34
fun run_sledgehammer (params as {blocking, debug, provers, full_types,
blanchet@40069
    35
                                 relevance_thresholds, max_relevant, ...})
blanchet@39366
    36
                     auto i (relevance_override as {only, ...}) minimize_command
blanchet@39366
    37
                     state =
blanchet@40059
    38
  if null provers then
blanchet@40059
    39
    error "No prover is set."
blanchet@39318
    40
  else case subgoal_count state of
wenzelm@40132
    41
    0 => (Output.urgent_message "No subgoal!"; (false, state))
blanchet@39318
    42
  | n =>
blanchet@39318
    43
    let
blanchet@39364
    44
      val _ = Proof.assert_backward state
blanchet@40200
    45
      val ctxt = Proof.context_of state
blanchet@40200
    46
      val {facts = chained_ths, goal, ...} = Proof.goal state
blanchet@40060
    47
      val (_, hyp_ts, concl_t) = strip_subgoal goal i
blanchet@40059
    48
      val _ = () |> not blocking ? kill_provers
blanchet@40941
    49
      val _ = case find_first (not o is_prover_available ctxt) provers of
blanchet@40941
    50
                SOME name => error ("No such prover: " ^ name ^ ".")
blanchet@40941
    51
              | NONE => ()
wenzelm@40132
    52
      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
blanchet@40941
    53
      val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
blanchet@40369
    54
      fun run_provers label full_types relevance_fudge maybe_translate provers
blanchet@40369
    55
                      (res as (success, state)) =
blanchet@40065
    56
        if success orelse null provers then
blanchet@40060
    57
          res
blanchet@40060
    58
        else
blanchet@40060
    59
          let
blanchet@40060
    60
            val max_max_relevant =
blanchet@40060
    61
              case max_relevant of
blanchet@40060
    62
                SOME n => n
blanchet@40060
    63
              | NONE =>
blanchet@40941
    64
                0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
blanchet@40065
    65
                          provers
blanchet@40060
    66
                  |> auto ? (fn n => n div auto_max_relevant_divisor)
blanchet@40369
    67
            val is_built_in_const =
blanchet@40369
    68
              is_built_in_const_for_prover ctxt (hd provers)
blanchet@40204
    69
            val facts =
blanchet@40065
    70
              relevant_facts ctxt full_types relevance_thresholds
blanchet@40369
    71
                             max_max_relevant is_built_in_const relevance_fudge
blanchet@40071
    72
                             relevance_override chained_ths hyp_ts concl_t
blanchet@40114
    73
              |> map maybe_translate
blanchet@40062
    74
            val problem =
blanchet@40065
    75
              {state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@40983
    76
               facts = facts}
blanchet@40983
    77
            val run_prover = run_prover params auto minimize_command only
blanchet@40060
    78
          in
blanchet@40205
    79
            if debug then
blanchet@40370
    80
              Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
blanchet@40205
    81
                  (if null facts then
blanchet@40205
    82
                     "Found no relevant facts."
blanchet@40205
    83
                   else
blanchet@40205
    84
                     "Including (up to) " ^ string_of_int (length facts) ^
blanchet@40205
    85
                     " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
blanchet@40205
    86
                     (facts |> map_filter fact_name
blanchet@40205
    87
                            |> space_implode " ") ^ "."))
blanchet@40205
    88
            else
blanchet@40205
    89
              ();
blanchet@40060
    90
            if auto then
blanchet@40061
    91
              fold (fn prover => fn (true, state) => (true, state)
blanchet@40064
    92
                                  | (false, _) => run_prover problem prover)
blanchet@40065
    93
                   provers (false, state)
blanchet@40060
    94
            else
blanchet@40065
    95
              provers |> (if blocking then Par_List.map else map)
blanchet@40065
    96
                             (run_prover problem)
blanchet@40065
    97
                      |> exists fst |> rpair state
blanchet@40060
    98
          end
blanchet@40071
    99
      val run_atps =
blanchet@40370
   100
        run_provers "ATP" full_types atp_relevance_fudge
blanchet@40204
   101
                    (Translated o translate_fact ctxt) atps
blanchet@40071
   102
      val run_smts =
blanchet@40370
   103
        run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
blanchet@40060
   104
      fun run_atps_and_smt_solvers () =
blanchet@40065
   105
        [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
blanchet@40060
   106
    in
blanchet@40065
   107
      (false, state)
blanchet@40065
   108
      |> (if blocking then run_atps #> not auto ? run_smts
blanchet@40065
   109
          else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
blanchet@40060
   110
    end
blanchet@38044
   111
wenzelm@28582
   112
end;