69 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
69 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
70 fun index_str (j, s) = s ^ "@" ^ string_of_int j |
70 fun index_str (j, s) = s ^ "@" ^ string_of_int j |
71 val str_of_method = enclose " " ": " |
71 val str_of_method = enclose " " ": " |
72 fun str_of_result method facts ({outcome, run_time, used_facts, ...} |
72 fun str_of_result method facts ({outcome, run_time, used_facts, ...} |
73 : prover_result) = |
73 : prover_result) = |
74 let val facts = facts |> map (fn ((name, _), _) => name ()) in |
74 let val facts = facts |> map (fst o fst) in |
75 str_of_method method ^ |
75 str_of_method method ^ |
76 (if is_none outcome then |
76 (if is_none outcome then |
77 "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ |
77 "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ |
78 (used_facts |> map (with_index facts o fst) |
78 (used_facts |> map (with_index facts o fst) |
79 |> sort (int_ord o pairself fst) |
79 |> sort (int_ord o pairself fst) |
109 | NONE => error ("No fact called \"" ^ name ^ "\".") |
109 | NONE => error ("No fact called \"" ^ name ^ "\".") |
110 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
110 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
111 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
111 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
112 val isar_deps = isar_dependencies_of name_tabs th |
112 val isar_deps = isar_dependencies_of name_tabs th |
113 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
113 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
114 val find_suggs = find_suggested_facts facts |
114 val find_suggs = find_suggested_facts facts #> map fact_of_raw_fact |
115 fun get_facts [] compute = compute facts |
115 fun get_facts [] compute = compute facts |
116 | get_facts suggs _ = find_suggs suggs |
116 | get_facts suggs _ = find_suggs suggs |
117 val mepo_facts = |
117 val mepo_facts = |
118 get_facts mepo_suggs (fn _ => |
118 get_facts mepo_suggs (fn _ => |
119 mepo_suggested_facts ctxt params prover slack_max_facts NONE |
119 mepo_suggested_facts ctxt params prover slack_max_facts NONE |
120 hyp_ts concl_t facts) |
120 hyp_ts concl_t facts) |
121 |> weight_mepo_facts |
121 |> weight_mepo_facts |
122 fun mash_of suggs = |
122 fun mash_of suggs = |
123 get_facts suggs (fn _ => |
123 get_facts suggs (fn _ => |
124 find_mash_suggestions slack_max_facts suggs facts [] [] |> fst) |
124 find_mash_suggestions slack_max_facts suggs facts [] [] |
|
125 |> fst |> map fact_of_raw_fact) |
125 |> weight_mash_facts |
126 |> weight_mash_facts |
126 val mash_isar_facts = mash_of mash_isar_suggs |
127 val mash_isar_facts = mash_of mash_isar_suggs |
127 val mash_prover_facts = mash_of mash_prover_suggs |
128 val mash_prover_facts = mash_of mash_prover_suggs |
128 fun mess_of mash_facts = |
129 fun mess_of mash_facts = |
129 [(mepo_weight, (mepo_facts, [])), |
130 [(mepo_weight, (mepo_facts, [])), |
158 val facts = |
159 val facts = |
159 facts |
160 facts |
160 |> map (get #> nickify) |
161 |> map (get #> nickify) |
161 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
162 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
162 |> take (the max_facts) |
163 |> take (the max_facts) |
|
164 |> map fact_of_raw_fact |
163 val ctxt = ctxt |> set_file_name method prob_dir_name |
165 val ctxt = ctxt |> set_file_name method prob_dir_name |
164 val res as {outcome, ...} = |
166 val res as {outcome, ...} = |
165 run_prover_for_mash ctxt params prover facts goal |
167 run_prover_for_mash ctxt params prover facts goal |
166 val ok = if is_none outcome then 1 else 0 |
168 val ok = if is_none outcome then 1 else 0 |
167 in (str_of_result method facts res, ok) end |
169 in (str_of_result method facts res, ok) end |