src/HOL/TPTP/mash_eval.ML
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63692 1bc4bc2c9fd1
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
     1 (*  Title:      HOL/TPTP/mash_eval.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2012
     4 
     5 Evaluate proof suggestions from MaSh (Machine-learning for Sledgehammer).
     6 *)
     7 
     8 signature MASH_EVAL =
     9 sig
    10   type params = Sledgehammer_Prover.params
    11 
    12   val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string option ->
    13     string list -> string -> unit
    14 end;
    15 
    16 structure MaSh_Eval : MASH_EVAL =
    17 struct
    18 
    19 open Sledgehammer_Util
    20 open Sledgehammer_Fact
    21 open Sledgehammer_MePo
    22 open Sledgehammer_MaSh
    23 open Sledgehammer_Prover
    24 open Sledgehammer_Prover_ATP
    25 open Sledgehammer_Commands
    26 open MaSh_Export
    27 
    28 val prefix = Library.prefix
    29 
    30 fun evaluate_mash_suggestions ctxt params range prob_dir_name file_names report_file_name =
    31   let
    32     val thy = Proof_Context.theory_of ctxt
    33     val zeros = [0, 0, 0, 0, 0, 0]
    34     val report_path = report_file_name |> Path.explode
    35     val _ = File.write report_path ""
    36 
    37     fun print s = File.append report_path (s ^ "\n")
    38 
    39     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
    40     val prover = hd provers
    41     val max_suggs = generous_max_suggestions (the max_facts)
    42 
    43     val method_of_file_name =
    44       perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/"
    45 
    46     val methods = "isar" :: map method_of_file_name file_names
    47     val lines_of = Path.explode #> try File.read_lines #> these
    48     val liness0 = map lines_of file_names
    49     val num_lines = fold (Integer.max o length) liness0 0
    50 
    51     fun pad lines = lines @ replicate (num_lines - length lines) ""
    52 
    53     val liness' = Ctr_Sugar_Util.transpose (map pad liness0)
    54 
    55     val css = clasimpset_rule_table_of ctxt
    56     val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css
    57     val name_tabs = build_name_tables nickname_of_thm facts
    58 
    59     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
    60     fun index_str (j, s) = s ^ "@" ^ string_of_int j
    61     val str_of_method = enclose "  " ": "
    62 
    63     fun str_of_result method facts ({outcome, run_time, used_facts, ...} : prover_result) =
    64       let val facts = facts |> map (fst o fst) in
    65         str_of_method method ^
    66         (if is_none outcome then
    67            "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^
    68            (used_facts |> map (with_index facts o fst)
    69                        |> sort (int_ord o apply2 fst)
    70                        |> map index_str
    71                        |> space_implode " ") ^
    72            (if length facts < the max_facts then
    73               " (of " ^ string_of_int (length facts) ^ ")"
    74             else
    75               "")
    76          else
    77            "Failure: " ^
    78            (facts |> take (the max_facts) |> tag_list 1
    79                   |> map index_str
    80                   |> space_implode " "))
    81       end
    82 
    83     fun solve_goal (j, lines) =
    84       if in_range range j andalso exists (curry (op <>) "") lines then
    85         let
    86           val get_suggs = extract_suggestions ##> (take max_suggs #> map fst)
    87           val (names, suggss0) = split_list (map get_suggs lines)
    88           val name =
    89             (case names |> filter (curry (op <>) "") |> distinct (op =) of
    90               [name] => name
    91             | names => error ("Input files out of sync: facts " ^ commas (map quote names)))
    92           val th =
    93             case find_first (fn (_, th) => nickname_of_thm th = name) facts of
    94               SOME (_, th) => th
    95             | NONE => error ("No fact called \"" ^ name)
    96           val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
    97           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
    98           val isar_deps = these (isar_dependencies_of name_tabs th)
    99           val suggss = isar_deps :: suggss0
   100           val facts = facts |> filter (fn (_, th') => thm_less (th', th))
   101 
   102           (* adapted from "mirabelle_sledgehammer.ML" *)
   103           fun set_file_name method (SOME dir) =
   104               let
   105                 val prob_prefix = "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ method
   106               in
   107                 Config.put atp_dest_dir dir
   108                 #> Config.put atp_problem_prefix (prob_prefix ^ "__")
   109                 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
   110               end
   111             | set_file_name _ NONE = I
   112 
   113           fun prove method suggs =
   114             if null facts then
   115               (str_of_method method ^ "Skipped", 0)
   116             else
   117               let
   118                 fun nickify ((_, stature), th) =
   119                   ((K (encode_str (nickname_of_thm th)), stature), th)
   120 
   121                 val facts =
   122                   suggs
   123                   |> find_suggested_facts ctxt facts
   124                   |> map (fact_of_raw_fact #> nickify)
   125                   |> maybe_instantiate_inducts ctxt hyp_ts concl_t
   126                   |> take (the max_facts)
   127                   |> map fact_of_raw_fact
   128                 val ctxt = ctxt |> set_file_name method prob_dir_name
   129                 val res as {outcome, ...} = run_prover_for_mash ctxt params prover name facts goal
   130                 val ok = if is_none outcome then 1 else 0
   131               in
   132                 (str_of_result method facts res, ok)
   133               end
   134 
   135           val ress = map2 prove methods suggss
   136         in
   137           "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
   138           |> cat_lines |> print;
   139           map snd ress
   140         end
   141       else
   142         zeros
   143 
   144     val inst_inducts = Config.get ctxt instantiate_inducts
   145     val options =
   146       ["prover = " ^ prover,
   147        "max_facts = " ^ string_of_int (the max_facts),
   148        "slice" |> not slice ? prefix "dont_",
   149        "type_enc = " ^ the_default "smart" type_enc,
   150        "lam_trans = " ^ the_default "smart" lam_trans,
   151        "timeout = " ^ ATP_Util.string_of_time timeout,
   152        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
   153     val _ = print " * * *";
   154     val _ = print ("Options: " ^ commas options);
   155     val oks = Par_List.map solve_goal (tag_list 1 liness')
   156     val n = length oks
   157 
   158     fun total_of method ok =
   159       str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1))
   160         (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
   161 
   162     val oks' = if n = 0 then zeros else map Integer.sum (map_transpose I oks)
   163   in
   164     "Successes (of " ^ string_of_int n ^ " goals)" ::
   165     map2 total_of methods oks'
   166     |> cat_lines |> print
   167   end
   168 
   169 end;