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