114 val facts = |
114 val facts = |
115 facts |
115 facts |
116 |> filter (fn (_, th') => |
116 |> filter (fn (_, th') => |
117 if linearize then crude_thm_ord (th', th) = LESS |
117 if linearize then crude_thm_ord (th', th) = LESS |
118 else thm_less (th', th)) |
118 else thm_less (th', th)) |
119 val find_suggs = |
|
120 find_suggested_facts ctxt facts #> map fact_of_raw_fact |
|
121 fun get_facts [] compute = compute facts |
|
122 | get_facts suggs _ = find_suggs suggs |
|
123 val mepo_facts = |
|
124 get_facts mepo_suggs (fn _ => |
|
125 mepo_suggested_facts ctxt params prover slack_max_facts NONE |
|
126 hyp_ts concl_t facts) |
|
127 |> weight_mepo_facts |
|
128 fun mash_of suggs = |
|
129 get_facts suggs (fn _ => |
|
130 find_mash_suggestions ctxt slack_max_facts suggs facts [] [] |
|
131 |> fst |> map fact_of_raw_fact) |
|
132 |> weight_mash_facts |
|
133 val mash_isar_facts = mash_of mash_isar_suggs |
|
134 val mash_prover_facts = mash_of mash_prover_suggs |
|
135 fun mess_of mash_facts = |
|
136 [(mepo_weight, (mepo_facts, [])), |
|
137 (mash_weight, (mash_facts, []))] |
|
138 fun mesh_of suggs mash_facts = |
|
139 get_facts suggs (fn _ => |
|
140 mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts |
|
141 (mess_of mash_facts)) |
|
142 val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts |
|
143 val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts |
|
144 val isar_facts = find_suggs isar_deps |
|
145 (* adapted from "mirabelle_sledgehammer.ML" *) |
119 (* adapted from "mirabelle_sledgehammer.ML" *) |
146 fun set_file_name method (SOME dir) = |
120 fun set_file_name method (SOME dir) = |
147 let |
121 let |
148 val prob_prefix = |
122 val prob_prefix = |
149 "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ |
123 "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ |
152 Config.put dest_dir dir |
126 Config.put dest_dir dir |
153 #> Config.put problem_prefix (prob_prefix ^ "__") |
127 #> Config.put problem_prefix (prob_prefix ^ "__") |
154 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) |
128 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) |
155 end |
129 end |
156 | set_file_name _ NONE = I |
130 | set_file_name _ NONE = I |
157 fun prove method get facts = |
131 fun prove method suggs = |
158 if not (member (op =) methods method) orelse |
132 if not (member (op =) methods method) orelse |
159 (null facts andalso method <> IsarN) then |
133 (null facts andalso method <> IsarN) then |
160 (str_of_method method ^ "Skipped", 0) |
134 (str_of_method method ^ "Skipped", 0) |
161 else |
135 else |
162 let |
136 let |
163 fun nickify ((_, stature), th) = |
137 fun nickify ((_, stature), th) = |
164 ((K (encode_str (nickname_of_thm th)), stature), th) |
138 ((K (encode_str (nickname_of_thm th)), stature), th) |
165 val facts = |
139 val facts = |
166 facts |
140 suggs |
167 |> map (get #> nickify) |
141 |> find_suggested_facts ctxt facts |
|
142 |> map (fact_of_raw_fact #> nickify) |
168 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
143 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
169 |> take (the max_facts) |
144 |> take (the max_facts) |
170 |> map fact_of_raw_fact |
145 |> map fact_of_raw_fact |
171 val ctxt = ctxt |> set_file_name method prob_dir_name |
146 val ctxt = ctxt |> set_file_name method prob_dir_name |
172 val res as {outcome, ...} = |
147 val res as {outcome, ...} = |
173 run_prover_for_mash ctxt params prover facts goal |
148 run_prover_for_mash ctxt params prover facts goal |
174 val ok = if is_none outcome then 1 else 0 |
149 val ok = if is_none outcome then 1 else 0 |
175 in (str_of_result method facts res, ok) end |
150 in (str_of_result method facts res, ok) end |
176 val ress = |
151 val ress = |
177 [fn () => prove MePoN fst mepo_facts, |
152 [fn () => prove MePoN mepo_suggs, |
178 fn () => prove MaSh_IsarN fst mash_isar_facts, |
153 fn () => prove MaSh_IsarN mash_isar_suggs, |
179 fn () => prove MaSh_ProverN fst mash_prover_facts, |
154 fn () => prove MaSh_ProverN mash_prover_suggs, |
180 fn () => prove MeSh_IsarN I mesh_isar_facts, |
155 fn () => prove MeSh_IsarN mesh_isar_suggs, |
181 fn () => prove MeSh_ProverN I mesh_prover_facts, |
156 fn () => prove MeSh_ProverN mesh_prover_suggs, |
182 fn () => prove IsarN I isar_facts] |
157 fn () => prove IsarN isar_deps] |
183 |> (* Par_List. *) map (fn f => f ()) |
158 |> (* Par_List. *) map (fn f => f ()) |
184 in |
159 in |
185 "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress |
160 "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress |
186 |> cat_lines |> print; |
161 |> cat_lines |> print; |
187 map snd ress |
162 map snd ress |