1.1 --- a/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 23:00:20 2013 +0100
1.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 23:29:17 2013 +0100
1.3 @@ -27,6 +27,7 @@
1.4 ML {*
1.5 val do_it = false (* switch to "true" to generate the files *)
1.6 val params = Sledgehammer_Isar.default_params @{context} []
1.7 +val range = (1, NONE)
1.8 val dir = "List"
1.9 val prefix = "/tmp/" ^ dir ^ "/"
1.10 val prob_dir = prefix ^ "mash_problems"
1.11 @@ -41,10 +42,15 @@
1.12
1.13 ML {*
1.14 if do_it then
1.15 - evaluate_mash_suggestions @{context} params (1, NONE)
1.16 + evaluate_mash_suggestions @{context} params range
1.17 [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
1.18 - (SOME prob_dir) (prefix ^ "mash_suggestions")
1.19 - (prefix ^ "mash_prover_suggestions") (prefix ^ "mash_eval")
1.20 + (SOME prob_dir)
1.21 + (prefix ^ "mepo_suggestions")
1.22 + (prefix ^ "mash_suggestions")
1.23 + (prefix ^ "mash_prover_suggestions")
1.24 + (prefix ^ "mesh_suggestions")
1.25 + (prefix ^ "mesh_prover_suggestions")
1.26 + (prefix ^ "mash_eval")
1.27 else
1.28 ()
1.29 *}
2.1 --- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 23:00:20 2013 +0100
2.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 23:29:17 2013 +0100
2.3 @@ -31,7 +31,7 @@
2.4 val prover = hd provers
2.5 val range = (1, NONE)
2.6 val step = 1
2.7 -val max_suggestions = 1536
2.8 +val max_suggestions = 1024
2.9 val dir = "List"
2.10 val prefix = "/tmp/" ^ dir ^ "/"
2.11 *}
3.1 --- a/src/HOL/TPTP/mash_eval.ML Thu Jan 17 23:00:20 2013 +0100
3.2 +++ b/src/HOL/TPTP/mash_eval.ML Thu Jan 17 23:29:17 2013 +0100
3.3 @@ -17,7 +17,7 @@
3.4 val IsarN : string
3.5 val evaluate_mash_suggestions :
3.6 Proof.context -> params -> int * int option -> string list -> string option
3.7 - -> string -> string -> string -> unit
3.8 + -> string -> string -> string -> string -> string -> string -> unit
3.9 end;
3.10
3.11 structure MaSh_Eval : MASH_EVAL =
3.12 @@ -41,7 +41,8 @@
3.13 j >= from andalso (to = NONE orelse j <= the to)
3.14
3.15 fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
3.16 - isar_sugg_file_name prover_sugg_file_name report_file_name =
3.17 + mepo_file_name mash_isar_file_name mash_prover_file_name
3.18 + mesh_isar_file_name mesh_prover_file_name report_file_name =
3.19 let
3.20 val report_path = report_file_name |> Path.explode
3.21 val _ = File.write report_path ""
3.22 @@ -50,12 +51,18 @@
3.23 default_params ctxt []
3.24 val prover = hd provers
3.25 val slack_max_facts = generous_max_facts (the max_facts)
3.26 - val mash_isar_lines = Path.explode isar_sugg_file_name |> File.read_lines
3.27 - val mash_prover_lines =
3.28 - case Path.explode prover_sugg_file_name |> try File.read_lines of
3.29 - NONE => replicate (length mash_isar_lines) ""
3.30 - | SOME lines => lines
3.31 - val mash_lines = mash_isar_lines ~~ mash_prover_lines
3.32 + val lines_of = Path.explode #> try File.read_lines #> these
3.33 + val file_names =
3.34 + [mepo_file_name, mash_isar_file_name, mash_prover_file_name,
3.35 + mesh_isar_file_name, mesh_prover_file_name]
3.36 + val lines as [mepo_lines, mash_isar_lines, mash_prover_lines,
3.37 + mesh_isar_lines, mesh_prover_lines] =
3.38 + map lines_of file_names
3.39 + val num_lines = fold (Integer.max o length) lines 0
3.40 + fun pad lines = lines @ replicate (num_lines - length lines) ""
3.41 + val lines =
3.42 + pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~
3.43 + pad mesh_isar_lines ~~ pad mesh_prover_lines
3.44 val css = clasimpset_rule_table_of ctxt
3.45 val facts = all_facts ctxt true false Symtab.empty [] [] css
3.46 val name_tabs = build_name_tables nickname_of_thm facts
3.47 @@ -82,11 +89,19 @@
3.48 |> map index_str
3.49 |> space_implode " "))
3.50 end
3.51 - fun solve_goal (j, (mash_isar_line, mash_prover_line)) =
3.52 + fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line),
3.53 + mesh_isar_line), mesh_prover_line)) =
3.54 if in_range range j then
3.55 let
3.56 - val (name, mash_isar_suggs) = extract_suggestions mash_isar_line
3.57 - val (_, mash_prover_suggs) = extract_suggestions mash_prover_line
3.58 + val (name1, mepo_suggs) = extract_suggestions mepo_line
3.59 + val (name2, mash_isar_suggs) = extract_suggestions mash_isar_line
3.60 + val (name3, mash_prover_suggs) = extract_suggestions mash_prover_line
3.61 + val (name4, mesh_isar_suggs) = extract_suggestions mesh_isar_line
3.62 + val (name5, mesh_prover_suggs) = extract_suggestions mesh_prover_line
3.63 + val [name] =
3.64 + [name1, name2, name3, name4, name5]
3.65 + |> filter (curry (op <>) "") |> distinct (op =)
3.66 + handle General.Match => error "Input files out of sync."
3.67 val th =
3.68 case find_first (fn (_, th) => nickname_of_thm th = name) facts of
3.69 SOME (_, th) => th
3.70 @@ -95,24 +110,29 @@
3.71 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
3.72 val isar_deps = isar_dependencies_of name_tabs th
3.73 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
3.74 + fun get_facts [] compute = compute facts
3.75 + | get_facts suggs _ = find_suggested_facts suggs facts
3.76 val mepo_facts =
3.77 - mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
3.78 - concl_t facts
3.79 - |> weight_mepo_facts
3.80 + get_facts mepo_suggs (fn _ =>
3.81 + mepo_suggested_facts ctxt params prover slack_max_facts NONE
3.82 + hyp_ts concl_t facts
3.83 + |> weight_mepo_facts)
3.84 fun mash_of suggs =
3.85 - find_mash_suggestions slack_max_facts suggs facts [] []
3.86 - |>> weight_mash_facts
3.87 - val (mash_isar_facts, mash_isar_unks) = mash_of mash_isar_suggs
3.88 - val (mash_prover_facts, mash_prover_unks) = mash_of mash_prover_suggs
3.89 - fun mess_of mash_facts mash_unks =
3.90 + get_facts suggs (fn _ =>
3.91 + find_mash_suggestions slack_max_facts suggs facts [] []
3.92 + |> fst |> weight_mash_facts)
3.93 + val mash_isar_facts = mash_of mash_isar_suggs
3.94 + val mash_prover_facts = mash_of mash_prover_suggs
3.95 + fun mess_of mash_facts =
3.96 [(mepo_weight, (mepo_facts, [])),
3.97 - (mash_weight, (mash_facts, mash_unks))]
3.98 - fun mesh_of [] _ = []
3.99 - | mesh_of mash_facts mash_unks =
3.100 - mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
3.101 - (mess_of mash_facts mash_unks)
3.102 - val mesh_isar_facts = mesh_of mash_isar_facts mash_isar_unks
3.103 - val mesh_prover_facts = mesh_of mash_prover_facts mash_prover_unks
3.104 + (mash_weight, (mash_facts, []))]
3.105 + fun mesh_of suggs mash_facts =
3.106 + get_facts suggs (fn _ =>
3.107 + mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
3.108 + (mess_of mash_facts)
3.109 + |> map (rpair 1.0))
3.110 + val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts
3.111 + val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts
3.112 val isar_facts =
3.113 find_suggested_facts (map (rpair 1.0) isar_deps) facts
3.114 (* adapted from "mirabelle_sledgehammer.ML" *)
3.115 @@ -127,7 +147,7 @@
3.116 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
3.117 end
3.118 | set_file_name _ NONE = I
3.119 - fun prove method get facts =
3.120 + fun prove method facts =
3.121 if not (member (op =) methods method) orelse
3.122 (null facts andalso method <> IsarN) then
3.123 (str_of_method method ^ "Skipped", 0)
3.124 @@ -137,7 +157,7 @@
3.125 ((K (encode_str (nickname_of_thm th)), stature), th)
3.126 val facts =
3.127 facts
3.128 - |> map (get #> nickify)
3.129 + |> map (fst #> nickify)
3.130 |> maybe_instantiate_inducts ctxt hyp_ts concl_t
3.131 |> take (the max_facts)
3.132 val ctxt = ctxt |> set_file_name method prob_dir_name
3.133 @@ -146,12 +166,12 @@
3.134 val ok = if is_none outcome then 1 else 0
3.135 in (str_of_result method facts res, ok) end
3.136 val ress =
3.137 - [fn () => prove MePoN fst mepo_facts,
3.138 - fn () => prove MaSh_IsarN fst mash_isar_facts,
3.139 - fn () => prove MaSh_ProverN fst mash_prover_facts,
3.140 - fn () => prove MeSh_IsarN I mesh_isar_facts,
3.141 - fn () => prove MeSh_ProverN I mesh_prover_facts,
3.142 - fn () => prove IsarN fst isar_facts]
3.143 + [fn () => prove MePoN mepo_facts,
3.144 + fn () => prove MaSh_IsarN mash_isar_facts,
3.145 + fn () => prove MaSh_ProverN mash_prover_facts,
3.146 + fn () => prove MeSh_IsarN mesh_isar_facts,
3.147 + fn () => prove MeSh_ProverN mesh_prover_facts,
3.148 + fn () => prove IsarN isar_facts]
3.149 |> (* Par_List. *) map (fn f => f ())
3.150 in
3.151 "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
3.152 @@ -175,7 +195,7 @@
3.153 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
3.154 val _ = print " * * *";
3.155 val _ = print ("Options: " ^ commas options);
3.156 - val oks = Par_List.map solve_goal (tag_list 1 mash_lines)
3.157 + val oks = Par_List.map solve_goal (tag_list 1 lines)
3.158 val n = length oks
3.159 val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok,
3.160 isar_ok] =