1.1 --- a/src/HOL/TPTP/mash_eval.ML Thu Jan 17 23:00:20 2013 +0100
1.2 +++ b/src/HOL/TPTP/mash_eval.ML Thu Jan 17 23:29:17 2013 +0100
1.3 @@ -17,7 +17,7 @@
1.4 val IsarN : string
1.5 val evaluate_mash_suggestions :
1.6 Proof.context -> params -> int * int option -> string list -> string option
1.7 - -> string -> string -> string -> unit
1.8 + -> string -> string -> string -> string -> string -> string -> unit
1.9 end;
1.10
1.11 structure MaSh_Eval : MASH_EVAL =
1.12 @@ -41,7 +41,8 @@
1.13 j >= from andalso (to = NONE orelse j <= the to)
1.14
1.15 fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
1.16 - isar_sugg_file_name prover_sugg_file_name report_file_name =
1.17 + mepo_file_name mash_isar_file_name mash_prover_file_name
1.18 + mesh_isar_file_name mesh_prover_file_name report_file_name =
1.19 let
1.20 val report_path = report_file_name |> Path.explode
1.21 val _ = File.write report_path ""
1.22 @@ -50,12 +51,18 @@
1.23 default_params ctxt []
1.24 val prover = hd provers
1.25 val slack_max_facts = generous_max_facts (the max_facts)
1.26 - val mash_isar_lines = Path.explode isar_sugg_file_name |> File.read_lines
1.27 - val mash_prover_lines =
1.28 - case Path.explode prover_sugg_file_name |> try File.read_lines of
1.29 - NONE => replicate (length mash_isar_lines) ""
1.30 - | SOME lines => lines
1.31 - val mash_lines = mash_isar_lines ~~ mash_prover_lines
1.32 + val lines_of = Path.explode #> try File.read_lines #> these
1.33 + val file_names =
1.34 + [mepo_file_name, mash_isar_file_name, mash_prover_file_name,
1.35 + mesh_isar_file_name, mesh_prover_file_name]
1.36 + val lines as [mepo_lines, mash_isar_lines, mash_prover_lines,
1.37 + mesh_isar_lines, mesh_prover_lines] =
1.38 + map lines_of file_names
1.39 + val num_lines = fold (Integer.max o length) lines 0
1.40 + fun pad lines = lines @ replicate (num_lines - length lines) ""
1.41 + val lines =
1.42 + pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~
1.43 + pad mesh_isar_lines ~~ pad mesh_prover_lines
1.44 val css = clasimpset_rule_table_of ctxt
1.45 val facts = all_facts ctxt true false Symtab.empty [] [] css
1.46 val name_tabs = build_name_tables nickname_of_thm facts
1.47 @@ -82,11 +89,19 @@
1.48 |> map index_str
1.49 |> space_implode " "))
1.50 end
1.51 - fun solve_goal (j, (mash_isar_line, mash_prover_line)) =
1.52 + fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line),
1.53 + mesh_isar_line), mesh_prover_line)) =
1.54 if in_range range j then
1.55 let
1.56 - val (name, mash_isar_suggs) = extract_suggestions mash_isar_line
1.57 - val (_, mash_prover_suggs) = extract_suggestions mash_prover_line
1.58 + val (name1, mepo_suggs) = extract_suggestions mepo_line
1.59 + val (name2, mash_isar_suggs) = extract_suggestions mash_isar_line
1.60 + val (name3, mash_prover_suggs) = extract_suggestions mash_prover_line
1.61 + val (name4, mesh_isar_suggs) = extract_suggestions mesh_isar_line
1.62 + val (name5, mesh_prover_suggs) = extract_suggestions mesh_prover_line
1.63 + val [name] =
1.64 + [name1, name2, name3, name4, name5]
1.65 + |> filter (curry (op <>) "") |> distinct (op =)
1.66 + handle General.Match => error "Input files out of sync."
1.67 val th =
1.68 case find_first (fn (_, th) => nickname_of_thm th = name) facts of
1.69 SOME (_, th) => th
1.70 @@ -95,24 +110,29 @@
1.71 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
1.72 val isar_deps = isar_dependencies_of name_tabs th
1.73 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
1.74 + fun get_facts [] compute = compute facts
1.75 + | get_facts suggs _ = find_suggested_facts suggs facts
1.76 val mepo_facts =
1.77 - mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
1.78 - concl_t facts
1.79 - |> weight_mepo_facts
1.80 + get_facts mepo_suggs (fn _ =>
1.81 + mepo_suggested_facts ctxt params prover slack_max_facts NONE
1.82 + hyp_ts concl_t facts
1.83 + |> weight_mepo_facts)
1.84 fun mash_of suggs =
1.85 - find_mash_suggestions slack_max_facts suggs facts [] []
1.86 - |>> weight_mash_facts
1.87 - val (mash_isar_facts, mash_isar_unks) = mash_of mash_isar_suggs
1.88 - val (mash_prover_facts, mash_prover_unks) = mash_of mash_prover_suggs
1.89 - fun mess_of mash_facts mash_unks =
1.90 + get_facts suggs (fn _ =>
1.91 + find_mash_suggestions slack_max_facts suggs facts [] []
1.92 + |> fst |> weight_mash_facts)
1.93 + val mash_isar_facts = mash_of mash_isar_suggs
1.94 + val mash_prover_facts = mash_of mash_prover_suggs
1.95 + fun mess_of mash_facts =
1.96 [(mepo_weight, (mepo_facts, [])),
1.97 - (mash_weight, (mash_facts, mash_unks))]
1.98 - fun mesh_of [] _ = []
1.99 - | mesh_of mash_facts mash_unks =
1.100 - mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
1.101 - (mess_of mash_facts mash_unks)
1.102 - val mesh_isar_facts = mesh_of mash_isar_facts mash_isar_unks
1.103 - val mesh_prover_facts = mesh_of mash_prover_facts mash_prover_unks
1.104 + (mash_weight, (mash_facts, []))]
1.105 + fun mesh_of suggs mash_facts =
1.106 + get_facts suggs (fn _ =>
1.107 + mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
1.108 + (mess_of mash_facts)
1.109 + |> map (rpair 1.0))
1.110 + val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts
1.111 + val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts
1.112 val isar_facts =
1.113 find_suggested_facts (map (rpair 1.0) isar_deps) facts
1.114 (* adapted from "mirabelle_sledgehammer.ML" *)
1.115 @@ -127,7 +147,7 @@
1.116 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
1.117 end
1.118 | set_file_name _ NONE = I
1.119 - fun prove method get facts =
1.120 + fun prove method facts =
1.121 if not (member (op =) methods method) orelse
1.122 (null facts andalso method <> IsarN) then
1.123 (str_of_method method ^ "Skipped", 0)
1.124 @@ -137,7 +157,7 @@
1.125 ((K (encode_str (nickname_of_thm th)), stature), th)
1.126 val facts =
1.127 facts
1.128 - |> map (get #> nickify)
1.129 + |> map (fst #> nickify)
1.130 |> maybe_instantiate_inducts ctxt hyp_ts concl_t
1.131 |> take (the max_facts)
1.132 val ctxt = ctxt |> set_file_name method prob_dir_name
1.133 @@ -146,12 +166,12 @@
1.134 val ok = if is_none outcome then 1 else 0
1.135 in (str_of_result method facts res, ok) end
1.136 val ress =
1.137 - [fn () => prove MePoN fst mepo_facts,
1.138 - fn () => prove MaSh_IsarN fst mash_isar_facts,
1.139 - fn () => prove MaSh_ProverN fst mash_prover_facts,
1.140 - fn () => prove MeSh_IsarN I mesh_isar_facts,
1.141 - fn () => prove MeSh_ProverN I mesh_prover_facts,
1.142 - fn () => prove IsarN fst isar_facts]
1.143 + [fn () => prove MePoN mepo_facts,
1.144 + fn () => prove MaSh_IsarN mash_isar_facts,
1.145 + fn () => prove MaSh_ProverN mash_prover_facts,
1.146 + fn () => prove MeSh_IsarN mesh_isar_facts,
1.147 + fn () => prove MeSh_ProverN mesh_prover_facts,
1.148 + fn () => prove IsarN isar_facts]
1.149 |> (* Par_List. *) map (fn f => f ())
1.150 in
1.151 "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
1.152 @@ -175,7 +195,7 @@
1.153 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
1.154 val _ = print " * * *";
1.155 val _ = print ("Options: " ^ commas options);
1.156 - val oks = Par_List.map solve_goal (tag_list 1 mash_lines)
1.157 + val oks = Par_List.map solve_goal (tag_list 1 lines)
1.158 val n = length oks
1.159 val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok,
1.160 isar_ok] =