110 slice = |
110 slice = |
111 let |
111 let |
112 val thy = Proof.theory_of state |
112 val thy = Proof.theory_of state |
113 val ctxt = Proof.context_of state |
113 val ctxt = Proof.context_of state |
114 |
114 |
115 val ATP_Slice ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans, |
115 val ((good_max_facts, good_fact_filter), SOME (good_format, good_type_enc, good_lam_trans, |
116 best_uncurried_aliases, extra) = slice |
116 good_uncurried_aliases, extra)) = slice |
117 |
117 |
118 val {exec, arguments, proof_delims, known_failures, prem_role, best_max_mono_iters, |
118 val {exec, arguments, proof_delims, known_failures, prem_role, good_max_mono_iters, |
119 best_max_new_mono_instances, ...} = get_atp thy name () |
119 good_max_new_mono_instances, ...} = get_atp thy name () |
120 |
120 |
121 val full_proofs = isar_proofs |> the_default (mode = Minimize) |
121 val full_proofs = isar_proofs |> the_default (mode = Minimize) |
122 val local_name = perhaps (try (unprefix remote_prefix)) name |
122 val local_name = perhaps (try (unprefix remote_prefix)) name |
123 |
123 |
124 val completish = Config.get ctxt atp_completish |
124 val completish = Config.get ctxt atp_completish |
164 let |
164 let |
165 fun monomorphize_facts facts = |
165 fun monomorphize_facts facts = |
166 let |
166 let |
167 val ctxt = |
167 val ctxt = |
168 ctxt |
168 ctxt |
169 |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances |
169 |> repair_monomorph_context max_mono_iters good_max_mono_iters max_new_mono_instances |
170 best_max_new_mono_instances |
170 good_max_new_mono_instances |
171 (* pseudo-theorem involving the same constants as the subgoal *) |
171 (* pseudo-theorem involving the same constants as the subgoal *) |
172 val subgoal_th = |
172 val subgoal_th = |
173 Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy |
173 Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy |
174 val rths = |
174 val rths = |
175 facts |> chop mono_max_privileged_facts |
175 facts |> chop mono_max_privileged_facts |
181 Monomorph.monomorph atp_schematic_consts_of ctxt rths |
181 Monomorph.monomorph atp_schematic_consts_of ctxt rths |
182 |> tl |> curry ListPair.zip (map fst facts) |
182 |> tl |> curry ListPair.zip (map fst facts) |
183 |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) |
183 |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) |
184 end |
184 end |
185 |
185 |
186 val effective_fact_filter = fact_filter |> the_default best_fact_filter |
186 val effective_fact_filter = fact_filter |> the_default good_fact_filter |
187 val facts = get_facts_of_filter effective_fact_filter factss |
187 val facts = get_facts_of_filter effective_fact_filter factss |
188 val num_facts = |
188 val num_facts = |
189 (case max_facts of |
189 (case max_facts of |
190 NONE => best_max_facts |
190 NONE => good_max_facts |
191 | SOME max_facts => max_facts) |
191 | SOME max_facts => max_facts) |
192 |> Integer.min (length facts) |
192 |> Integer.min (length facts) |
193 val strictness = if strict then Strict else Non_Strict |
193 val strictness = if strict then Strict else Non_Strict |
194 val type_enc = type_enc |> choose_type_enc strictness best_type_enc format |
194 val type_enc = type_enc |> choose_type_enc strictness good_type_enc good_format |
195 val run_timeout = slice_timeout slices timeout |
195 val run_timeout = slice_timeout slices timeout |
196 val generous_run_timeout = if mode = MaSh then one_day else run_timeout |
196 val generous_run_timeout = if mode = MaSh then one_day else run_timeout |
197 val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => |
197 val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => |
198 let |
198 let |
199 val sound = is_type_enc_sound type_enc |
199 val sound = is_type_enc_sound type_enc |
200 val generate_info = (case format of DFG _ => true | _ => false) |
200 val generate_info = (case good_format of DFG _ => true | _ => false) |
201 val readable_names = not (Config.get ctxt atp_full_names) |
201 val readable_names = not (Config.get ctxt atp_full_names) |
202 val lam_trans = lam_trans |> the_default best_lam_trans |
202 val lam_trans = lam_trans |> the_default good_lam_trans |
203 val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases |
203 val uncurried_aliases = uncurried_aliases |> the_default good_uncurried_aliases |
204 in |
204 in |
205 facts |
205 facts |
206 |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |
206 |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |
207 |> take num_facts |
207 |> take num_facts |
208 |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |
208 |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |
209 |> map (apsnd Thm.prop_of) |
209 |> map (apsnd Thm.prop_of) |
210 |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode |
210 |> generate_atp_problem ctxt generate_info good_format prem_role type_enc atp_mode |
211 lam_trans uncurried_aliases readable_names true hyp_ts concl_t |
211 lam_trans uncurried_aliases readable_names true hyp_ts concl_t |
212 end) () |
212 end) () |
213 |
213 |
214 val () = spying spy (fn () => |
214 val () = spying spy (fn () => |
215 (state, subgoal, name, "Generating ATP problem in " ^ |
215 (state, subgoal, name, "Generating ATP problem in " ^ |
231 let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) |
231 let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) |
232 in (Process_Result.out res, Process_Result.timing_elapsed res) end |
232 in (Process_Result.out res, Process_Result.timing_elapsed res) end |
233 |
233 |
234 val _ = |
234 val _ = |
235 atp_problem |
235 atp_problem |
236 |> lines_of_atp_problem format ord ord_info |
236 |> lines_of_atp_problem good_format ord ord_info |
237 |> (exec <> isabelle_scala_function) ? |
237 |> (exec <> isabelle_scala_function) ? |
238 cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |
238 cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |
239 |> File.write_list prob_path |
239 |> File.write_list prob_path |
240 |
240 |
241 val ((output, run_time), (atp_proof, outcome)) = |
241 val ((output, run_time), (atp_proof, outcome)) = |
266 if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure |
266 if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure |
267 end |
267 end |
268 | NONE => (found_proof name; NONE)) |
268 | NONE => (found_proof name; NONE)) |
269 | _ => outcome) |
269 | _ => outcome) |
270 in |
270 in |
271 (atp_problem_data, (output, run_time, facts, atp_proof, outcome), (format, type_enc)) |
271 (atp_problem_data, (output, run_time, facts, atp_proof, outcome), (good_format, type_enc)) |
272 end |
272 end |
273 |
273 |
274 (* If the problem file has not been exported, remove it; otherwise, export |
274 (* If the problem file has not been exported, remove it; otherwise, export |
275 the proof file too. *) |
275 the proof file too. *) |
276 fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () |
276 fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () |