16 type minimize_command = ATP_Reconstruct.minimize_command |
16 type minimize_command = ATP_Reconstruct.minimize_command |
17 type relevance_fudge = Sledgehammer_Filter.relevance_fudge |
17 type relevance_fudge = Sledgehammer_Filter.relevance_fudge |
18 |
18 |
19 datatype mode = Auto_Try | Try | Normal | Minimize |
19 datatype mode = Auto_Try | Try | Normal | Minimize |
20 |
20 |
21 datatype rich_type_sys = |
|
22 Dumb_Type_Sys of type_sys | |
|
23 Smart_Type_Sys of bool |
|
24 |
|
25 type params = |
21 type params = |
26 {debug: bool, |
22 {debug: bool, |
27 verbose: bool, |
23 verbose: bool, |
28 overlord: bool, |
24 overlord: bool, |
29 blocking: bool, |
25 blocking: bool, |
30 provers: string list, |
26 provers: string list, |
31 type_sys: rich_type_sys, |
27 type_sys: type_sys option, |
32 relevance_thresholds: real * real, |
28 relevance_thresholds: real * real, |
33 max_relevant: int option, |
29 max_relevant: int option, |
34 max_mono_iters: int, |
30 max_mono_iters: int, |
35 max_new_mono_instances: int, |
31 max_new_mono_instances: int, |
36 isar_proof: bool, |
32 isar_proof: bool, |
284 fun running_provers () = Async_Manager.running_threads das_tool "prover" |
280 fun running_provers () = Async_Manager.running_threads das_tool "prover" |
285 val messages = Async_Manager.thread_messages das_tool "prover" |
281 val messages = Async_Manager.thread_messages das_tool "prover" |
286 |
282 |
287 (** problems, results, ATPs, etc. **) |
283 (** problems, results, ATPs, etc. **) |
288 |
284 |
289 datatype rich_type_sys = |
|
290 Dumb_Type_Sys of type_sys | |
|
291 Smart_Type_Sys of bool |
|
292 |
|
293 type params = |
285 type params = |
294 {debug: bool, |
286 {debug: bool, |
295 verbose: bool, |
287 verbose: bool, |
296 overlord: bool, |
288 overlord: bool, |
297 blocking: bool, |
289 blocking: bool, |
298 provers: string list, |
290 provers: string list, |
299 type_sys: rich_type_sys, |
291 type_sys: type_sys option, |
300 relevance_thresholds: real * real, |
292 relevance_thresholds: real * real, |
301 max_relevant: int option, |
293 max_relevant: int option, |
302 max_mono_iters: int, |
294 max_mono_iters: int, |
303 max_new_mono_instances: int, |
295 max_new_mono_instances: int, |
304 isar_proof: bool, |
296 isar_proof: bool, |
508 |
500 |
509 (* Important messages are important but not so important that users want to see |
501 (* Important messages are important but not so important that users want to see |
510 them each time. *) |
502 them each time. *) |
511 val atp_important_message_keep_quotient = 10 |
503 val atp_important_message_keep_quotient = 10 |
512 |
504 |
513 val fallback_best_type_syss = |
505 fun choose_format_and_type_sys best_type_sys formats type_sys_opt = |
514 [Preds (Mangled_Monomorphic, Noninf_Nonmono_Types, Lightweight)] |
506 (case type_sys_opt of |
515 |
507 SOME ts => ts |
516 fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = |
508 | NONE => type_sys_from_string best_type_sys) |
517 choose_format formats type_sys |
509 |> choose_format formats |
518 | choose_format_and_type_sys best_type_syss formats |
|
519 (Smart_Type_Sys full_types) = |
|
520 map type_sys_from_string best_type_syss @ fallback_best_type_syss |
|
521 |> find_first (if full_types then is_type_sys_virtually_sound else K true) |
|
522 |> the |> choose_format formats |
|
523 |
510 |
524 val metis_minimize_max_time = seconds 2.0 |
511 val metis_minimize_max_time = seconds 2.0 |
525 |
512 |
526 fun choose_minimize_command minimize_command name preplay = |
513 fun choose_minimize_command minimize_command name preplay = |
527 (case preplay of |
514 (case preplay of |
607 |> fst |> tl |
594 |> fst |> tl |
608 |> curry ListPair.zip (map fst facts) |
595 |> curry ListPair.zip (map fst facts) |
609 |> maps (fn (name, rths) => map (pair name o snd) rths) |
596 |> maps (fn (name, rths) => map (pair name o snd) rths) |
610 end |
597 end |
611 fun run_slice (slice, (time_frac, (complete, |
598 fun run_slice (slice, (time_frac, (complete, |
612 (best_max_relevant, best_type_syss, extra)))) |
599 (best_max_relevant, best_type_sys, extra)))) |
613 time_left = |
600 time_left = |
614 let |
601 let |
615 val num_facts = |
602 val num_facts = |
616 length facts |> is_none max_relevant |
603 length facts |> is_none max_relevant |
617 ? Integer.min best_max_relevant |
604 ? Integer.min best_max_relevant |
618 val (format, type_sys) = |
605 val (format, type_sys) = |
619 choose_format_and_type_sys best_type_syss formats type_sys |
606 choose_format_and_type_sys best_type_sys formats type_sys |
620 val fairly_sound = is_type_sys_fairly_sound type_sys |
607 val fairly_sound = is_type_sys_fairly_sound type_sys |
621 val facts = |
608 val facts = |
622 facts |> map untranslated_fact |
609 facts |> map untranslated_fact |
623 |> not fairly_sound |
610 |> not fairly_sound |
624 ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |
611 ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |