equal
deleted
inserted
replaced
529 |> timed_reconstructor |
529 |> timed_reconstructor |
530 |>> log o prefix (reconstructor_tag reconstructor id) |
530 |>> log o prefix (reconstructor_tag reconstructor id) |
531 |> snd |
531 |> snd |
532 end |
532 end |
533 |
533 |
534 val try_inner_timeout = seconds 5.0 |
534 val try_timeout = seconds 5.0 |
535 val try_outer_timeout = seconds 30.0 |
|
536 |
535 |
537 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = |
536 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = |
538 let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in |
537 let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in |
539 if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal |
538 if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal |
540 then () else |
539 then () else |
542 val reconstructor = Unsynchronized.ref "" |
541 val reconstructor = Unsynchronized.ref "" |
543 val named_thms = |
542 val named_thms = |
544 Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) |
543 Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) |
545 val minimize = AList.defined (op =) args minimizeK |
544 val minimize = AList.defined (op =) args minimizeK |
546 val metis_ft = AList.defined (op =) args metis_ftK |
545 val metis_ft = AList.defined (op =) args metis_ftK |
547 val trivial = |
546 val trivial = Try.invoke_try (SOME try_timeout) pre |
548 TimeLimit.timeLimit try_outer_timeout |
547 handle TimeLimit.TimeOut => false |
549 (Try.invoke_try (SOME try_inner_timeout)) pre |
|
550 handle TimeLimit.TimeOut => false |
|
551 fun apply_reconstructor m1 m2 = |
548 fun apply_reconstructor m1 m2 = |
552 if metis_ft |
549 if metis_ft |
553 then |
550 then |
554 if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false |
551 if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false |
555 (run_reconstructor trivial false m1 name reconstructor |
552 (run_reconstructor trivial false m1 name reconstructor |