567 ("timeout", timeout |> Time.toSeconds |> string_of_int)] |
567 ("timeout", timeout |> Time.toSeconds |> string_of_int)] |
568 |
568 |
569 fun run_reconstructor trivial full m name reconstructor named_thms id |
569 fun run_reconstructor trivial full m name reconstructor named_thms id |
570 ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = |
570 ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = |
571 let |
571 let |
572 fun do_reconstructor thms ctxt = |
572 fun do_reconstructor named_thms ctxt = |
573 (if !reconstructor = "sledgehammer_tac" then |
573 let |
574 (fn ctxt => fn thms => |
574 val ref_of_str = |
575 Method.insert_tac thms THEN' |
575 suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm |
576 (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
576 #> fst |
577 (e_override_params timeout) |
577 val thms = named_thms |> maps snd |
578 ORELSE' |
578 val facts = named_thms |> map (ref_of_str o fst o fst) |
579 Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
579 val relevance_override = {add = facts, del = [], only = true} |
580 (vampire_override_params timeout))) |
580 in |
581 else if !reconstructor = "smt" then |
581 if !reconstructor = "sledgehammer_tac" then |
582 SMT_Solver.smt_tac |
582 Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
583 else if full orelse !reconstructor = "metis (full_types)" then |
583 (e_override_params timeout) relevance_override |
584 Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] |
584 ORELSE' |
585 else if !reconstructor = "metis (no_types)" then |
585 Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
586 Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] |
586 (vampire_override_params timeout) relevance_override |
587 else if !reconstructor = "metis" then |
587 else if !reconstructor = "smt" then |
588 Metis_Tactics.metis_tac [] |
588 SMT_Solver.smt_tac ctxt thms |
589 else |
589 else if full orelse !reconstructor = "metis (full_types)" then |
590 K (K (K all_tac))) ctxt thms |
590 Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] ctxt thms |
591 fun apply_reconstructor thms = |
591 else if !reconstructor = "metis (no_types)" then |
592 Mirabelle.can_apply timeout (do_reconstructor thms) st |
592 Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] ctxt thms |
|
593 else if !reconstructor = "metis" then |
|
594 Metis_Tactics.metis_tac [] ctxt thms |
|
595 else |
|
596 K all_tac |
|
597 end |
|
598 fun apply_reconstructor named_thms = |
|
599 Mirabelle.can_apply timeout (do_reconstructor named_thms) st |
593 |
600 |
594 fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" |
601 fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" |
595 | with_time (true, t) = (change_data id (inc_reconstructor_success m); |
602 | with_time (true, t) = (change_data id (inc_reconstructor_success m); |
596 if trivial then () |
603 if trivial then () |
597 else change_data id (inc_reconstructor_nontriv_success m); |
604 else change_data id (inc_reconstructor_nontriv_success m); |
599 change_data id (inc_reconstructor_time m t); |
606 change_data id (inc_reconstructor_time m t); |
600 change_data id (inc_reconstructor_posns m (pos, trivial)); |
607 change_data id (inc_reconstructor_posns m (pos, trivial)); |
601 if name = "proof" then change_data id (inc_reconstructor_proofs m) |
608 if name = "proof" then change_data id (inc_reconstructor_proofs m) |
602 else (); |
609 else (); |
603 "succeeded (" ^ string_of_int t ^ ")") |
610 "succeeded (" ^ string_of_int t ^ ")") |
604 fun timed_reconstructor thms = |
611 fun timed_reconstructor named_thms = |
605 (with_time (Mirabelle.cpu_time apply_reconstructor thms), true) |
612 (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true) |
606 handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); |
613 handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); |
607 ("timeout", false)) |
614 ("timeout", false)) |
608 | ERROR msg => ("error: " ^ msg, false) |
615 | ERROR msg => ("error: " ^ msg, false) |
609 |
616 |
610 val _ = log separator |
617 val _ = log separator |
611 val _ = change_data id (inc_reconstructor_calls m) |
618 val _ = change_data id (inc_reconstructor_calls m) |
612 val _ = if trivial then () |
619 val _ = if trivial then () |
613 else change_data id (inc_reconstructor_nontriv_calls m) |
620 else change_data id (inc_reconstructor_nontriv_calls m) |
614 in |
621 in |
615 maps snd named_thms |
622 named_thms |
616 |> timed_reconstructor |
623 |> timed_reconstructor |
617 |>> log o prefix (reconstructor_tag reconstructor id) |
624 |>> log o prefix (reconstructor_tag reconstructor id) |
618 |> snd |
625 |> snd |
619 end |
626 end |
620 |
627 |